LeanPool.ZFLean.IsomorphismsFunsToPowRel

Imported Lean Pool material for LeanPool.ZFLean.IsomorphismsFunsToPowRel.

@[reducible, inline]

noncomputable abbrev ZFSet.funsToPowRelF (A B : ZFSet.{u_1}) : ZFSet.{u_1}

Sends a function A → 𝒫 B to the corresponding relation on A × B.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev ZFSet.funsToPowRelG (A B : ZFSet.{u_1}) : ZFSet.{u_1}

Sends a relation on A × B to the corresponding function A → 𝒫 B.

Equations

• One or more equations did not get rendered due to their size.

theorem ZFSet.funsToPowRelF_isFunc {A B : ZFSet.{u_1}} : (A.funs B.powerset).IsFunc (A.prod B).powerset (A.funsToPowRelF B)

theorem ZFSet.funsToPowRelG_isFunc {A B : ZFSet.{u_1}} : (A.prod B).powerset.IsFunc (A.funs B.powerset) (A.funsToPowRelG B)

theorem ZFSet.funsToPowRel_left_inverse {A B : ZFSet.{u_1}} : (A.funsToPowRelG B ∘ᶻ A.funsToPowRelF B) ⋯ ⋯ = 𝟙(A.funs B.powerset)

theorem ZFSet.funsToPowRel_right_inverse {A B : ZFSet.{u_1}} : (A.funsToPowRelF B ∘ᶻ A.funsToPowRelG B) ⋯ ⋯ = 𝟙(A.prod B).powerset

theorem ZFSet.isIso_funs_to_pow_rel {A B : ZFSet.{u_1}} : A.funs B.powerset ≅ᶻ (A.prod B).powerset