Complete lattice homomorphisms #
This file defines frame homomorphisms and complete lattice homomorphisms.
We use the DFunLike design, so each type of morphisms has a companion typeclass which is meant to
be satisfied by itself and all stricter types.
Types of morphisms #
sSupHom: Maps which preserve⨆.sInfHom: Maps which preserve⨅.FrameHom: Frame homomorphisms. Maps which preserve⨆,⊓and⊤.CompleteLatticeHom: Complete lattice homomorphisms. Maps which preserve⨆and⨅.
Typeclasses #
Concrete homs #
CompleteLatticeHom.setPreimage:Set.preimageas a complete lattice homomorphism.
TODO #
Frame homs are Heyting homs.
The type of ⨆-preserving functions from α to β.
- toFun : α → β
The underlying function of a sSupHom.
The proposition that a
sSupHomcommutes with arbitrary suprema/joins.
The type of ⨅-preserving functions from α to β.
structure
FrameHom
(α : Type u_8)
(β : Type u_9)
[CompleteLattice α]
[CompleteLattice β]
extends InfTopHom α β :
Type (max u_8 u_9)
The type of frame homomorphisms from α to β. They preserve finite meets and arbitrary joins.
- toFun : α → β
The proposition that frame homomorphisms commute with arbitrary suprema/joins.
structure
CompleteLatticeHom
(α : Type u_8)
(β : Type u_9)
[CompleteLattice α]
[CompleteLattice β]
extends sInfHom α β :
Type (max u_8 u_9)
The type of complete lattice homomorphisms from α to β.
- toFun : α → β
The proposition that complete lattice homomorphism commutes with arbitrary suprema/joins.
class
sSupHomClass
(F : Type u_8)
(α : Type u_9)
(β : Type u_10)
[SupSet α]
[SupSet β]
[FunLike F α β]
:
sSupHomClass F α β states that F is a type of ⨆-preserving morphisms.
You should extend this class when you extend sSupHom.
The proposition that members of
sSupHomClasss commute with arbitrary suprema/joins.
class
sInfHomClass
(F : Type u_8)
(α : Type u_9)
(β : Type u_10)
[InfSet α]
[InfSet β]
[FunLike F α β]
:
sInfHomClass F α β states that F is a type of ⨅-preserving morphisms.
You should extend this class when you extend sInfHom.
The proposition that members of
sInfHomClasss commute with arbitrary infima/meets.
class
FrameHomClass
(F : Type u_8)
(α : Type u_9)
(β : Type u_10)
[CompleteLattice α]
[CompleteLattice β]
[FunLike F α β]
extends InfTopHomClass F α β :
FrameHomClass F α β states that F is a type of frame morphisms. They preserve ⊓ and ⨆.
You should extend this class when you extend FrameHom.
The proposition that members of
FrameHomClasscommute with arbitrary suprema/joins.
class
CompleteLatticeHomClass
(F : Type u_8)
(α : Type u_9)
(β : Type u_10)
[CompleteLattice α]
[CompleteLattice β]
[FunLike F α β]
extends sInfHomClass F α β :
CompleteLatticeHomClass F α β states that F is a type of complete lattice morphisms.
You should extend this class when you extend CompleteLatticeHom.
The proposition that members of
CompleteLatticeHomClasscommute with arbitrary suprema/joins.
@[instance 100]
instance
sSupHomClass.toSupBotHomClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[FunLike F α β]
[CompleteLattice α]
[CompleteLattice β]
[sSupHomClass F α β]
:
SupBotHomClass F α β
@[instance 100]
instance
sInfHomClass.toInfTopHomClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[FunLike F α β]
[CompleteLattice α]
[CompleteLattice β]
[sInfHomClass F α β]
:
InfTopHomClass F α β
@[instance 100]
instance
FrameHomClass.tosSupHomClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[FunLike F α β]
[CompleteLattice α]
[CompleteLattice β]
[FrameHomClass F α β]
:
sSupHomClass F α β
@[instance 100]
instance
FrameHomClass.toBoundedLatticeHomClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[FunLike F α β]
[CompleteLattice α]
[CompleteLattice β]
[FrameHomClass F α β]
:
BoundedLatticeHomClass F α β
@[instance 100]
instance
CompleteLatticeHomClass.toFrameHomClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[FunLike F α β]
[CompleteLattice α]
[CompleteLattice β]
[CompleteLatticeHomClass F α β]
:
FrameHomClass F α β
@[instance 100]
instance
CompleteLatticeHomClass.toBoundedLatticeHomClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[FunLike F α β]
[CompleteLattice α]
[CompleteLattice β]
[CompleteLatticeHomClass F α β]
:
BoundedLatticeHomClass F α β
@[instance 100]
instance
OrderIsoClass.tosSupHomClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[EquivLike F α β]
[CompleteLattice α]
[CompleteLattice β]
[OrderIsoClass F α β]
:
sSupHomClass F α β
@[instance 100]
instance
OrderIsoClass.tosInfHomClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[EquivLike F α β]
[CompleteLattice α]
[CompleteLattice β]
[OrderIsoClass F α β]
:
sInfHomClass F α β
@[instance 100]
instance
OrderIsoClass.toCompleteLatticeHomClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[EquivLike F α β]
[CompleteLattice α]
[CompleteLattice β]
[OrderIsoClass F α β]
:
CompleteLatticeHomClass F α β
def
OrderIso.toCompleteLatticeHom
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : α ≃o β)
:
Reinterpret an order isomorphism as a morphism of complete lattices.
Equations
- f.toCompleteLatticeHom = { toFun := ⇑f, map_sInf' := ⋯, map_sSup' := ⋯ }
@[simp]
theorem
OrderIso.toCompleteLatticeHom_toFun
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : α ≃o β)
(a : α)
:
instance
instCoeTCSSupHomOfSSupHomClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[FunLike F α β]
[SupSet α]
[SupSet β]
[sSupHomClass F α β]
:
Equations
- instCoeTCSSupHomOfSSupHomClass = { coe := fun (f : F) => { toFun := ⇑f, map_sSup' := ⋯ } }
instance
instCoeTCSInfHomOfSInfHomClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[FunLike F α β]
[InfSet α]
[InfSet β]
[sInfHomClass F α β]
:
Equations
- instCoeTCSInfHomOfSInfHomClass = { coe := fun (f : F) => { toFun := ⇑f, map_sInf' := ⋯ } }
instance
instCoeTCFrameHomOfFrameHomClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[FunLike F α β]
[CompleteLattice α]
[CompleteLattice β]
[FrameHomClass F α β]
:
Equations
- instCoeTCFrameHomOfFrameHomClass = { coe := fun (f : F) => { toFun := ⇑f, map_inf' := ⋯, map_top' := ⋯, map_sSup' := ⋯ } }
instance
instCoeTCCompleteLatticeHomOfCompleteLatticeHomClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[FunLike F α β]
[CompleteLattice α]
[CompleteLattice β]
[CompleteLatticeHomClass F α β]
:
CoeTC F (CompleteLatticeHom α β)
Equations
- instCoeTCCompleteLatticeHomOfCompleteLatticeHomClass = { coe := fun (f : F) => { toFun := ⇑f, map_sInf' := ⋯, map_sSup' := ⋯ } }
Supremum homomorphisms #
Equations
- sSupHom.instFunLike = { coe := sSupHom.toFun, coe_injective' := ⋯ }
instance
sSupHom.instSSupHomClass
{α : Type u_2}
{β : Type u_3}
[SupSet α]
[SupSet β]
:
sSupHomClass (sSupHom α β) α β
Equations
- sSupHom.id α = { toFun := id, map_sSup' := ⋯ }
Equations
- sSupHom.instInhabited α = { default := sSupHom.id α }
instance
sSupHom.instPartialOrder
{α : Type u_2}
{β : Type u_3}
[SupSet α]
{x✝ : CompleteLattice β}
:
PartialOrder (sSupHom α β)
Equations
- sSupHom.instPartialOrder = PartialOrder.lift (fun (f : sSupHom α β) => ⇑f) ⋯
Equations
- sSupHom.instBot = { bot := { toFun := fun (x : α) => ⊥, map_sSup' := ⋯ } }
Equations
@[simp]
@[simp]
theorem
sSupHom.bot_apply
{α : Type u_2}
{β : Type u_3}
[SupSet α]
{x✝ : CompleteLattice β}
(a : α)
:
Infimum homomorphisms #
Equations
- sInfHom.instFunLike = { coe := sInfHom.toFun, coe_injective' := ⋯ }
instance
sInfHom.instSInfHomClass
{α : Type u_2}
{β : Type u_3}
[InfSet α]
[InfSet β]
:
sInfHomClass (sInfHom α β) α β
Equations
- sInfHom.id α = { toFun := id, map_sInf' := ⋯ }
Equations
- sInfHom.instInhabited α = { default := sInfHom.id α }
instance
sInfHom.instPartialOrder
{α : Type u_2}
{β : Type u_3}
[InfSet α]
[CompleteLattice β]
:
PartialOrder (sInfHom α β)
Equations
- sInfHom.instPartialOrder = PartialOrder.lift (fun (f : sInfHom α β) => ⇑f) ⋯
Equations
- sInfHom.instTop = { top := { toFun := fun (x : α) => ⊤, map_sInf' := ⋯ } }
Equations
@[simp]
@[simp]
Frame homomorphisms #
instance
FrameHom.instFunLike
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
:
Equations
- FrameHom.instFunLike = { coe := fun (f : FrameHom α β) => f.toFun, coe_injective' := ⋯ }
instance
FrameHom.instFrameHomClass
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
:
FrameHomClass (FrameHom α β) α β
def
FrameHom.toLatticeHom
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : FrameHom α β)
:
LatticeHom α β
Reinterpret a FrameHom as a LatticeHom.
Equations
- f.toLatticeHom = { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ }
theorem
FrameHom.toFun_eq_coe
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : FrameHom α β)
:
@[simp]
theorem
FrameHom.coe_toInfTopHom
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : FrameHom α β)
:
@[simp]
theorem
FrameHom.coe_toLatticeHom
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : FrameHom α β)
:
@[simp]
theorem
FrameHom.coe_mk
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : InfTopHom α β)
(hf : ∀ (s : Set α), f.toFun (sSup s) = sSup (f.toFun '' s))
:
theorem
FrameHom.ext
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
{f g : FrameHom α β}
(h : ∀ (a : α), f a = g a)
:
def
FrameHom.copy
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : FrameHom α β)
(f' : α → β)
(h : f' = ⇑f)
:
FrameHom α β
Copy of a FrameHom with a new toFun equal to the old one. Useful to fix definitional
equalities.
@[simp]
theorem
FrameHom.coe_copy
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : FrameHom α β)
(f' : α → β)
(h : f' = ⇑f)
:
theorem
FrameHom.copy_eq
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : FrameHom α β)
(f' : α → β)
(h : f' = ⇑f)
:
Equations
- FrameHom.id α = { toInfTopHom := InfTopHom.id α, map_sSup' := ⋯ }
Equations
- FrameHom.instInhabited α = { default := FrameHom.id α }
@[simp]
def
FrameHom.comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
(f : FrameHom β γ)
(g : FrameHom α β)
:
FrameHom α γ
Composition of FrameHoms as a FrameHom.
Equations
- f.comp g = { toInfTopHom := f.comp g.toInfTopHom, map_sSup' := ⋯ }
@[simp]
theorem
FrameHom.coe_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
(f : FrameHom β γ)
(g : FrameHom α β)
:
@[simp]
theorem
FrameHom.comp_apply
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
(f : FrameHom β γ)
(g : FrameHom α β)
(a : α)
:
@[simp]
theorem
FrameHom.comp_assoc
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
{δ : Type u_5}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
[CompleteLattice δ]
(f : FrameHom γ δ)
(g : FrameHom β γ)
(h : FrameHom α β)
:
@[simp]
theorem
FrameHom.comp_id
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : FrameHom α β)
:
@[simp]
theorem
FrameHom.id_comp
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : FrameHom α β)
:
@[simp]
theorem
FrameHom.cancel_right
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
{g₁ g₂ : FrameHom β γ}
{f : FrameHom α β}
(hf : Function.Surjective ⇑f)
:
@[simp]
theorem
FrameHom.cancel_left
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
{g : FrameHom β γ}
{f₁ f₂ : FrameHom α β}
(hg : Function.Injective ⇑g)
:
instance
FrameHom.instPartialOrder
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
:
PartialOrder (FrameHom α β)
Equations
- FrameHom.instPartialOrder = PartialOrder.lift (fun (f : FrameHom α β) => ⇑f) ⋯
Complete lattice homomorphisms #
instance
CompleteLatticeHom.instFunLike
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
:
FunLike (CompleteLatticeHom α β) α β
Equations
- CompleteLatticeHom.instFunLike = { coe := fun (f : CompleteLatticeHom α β) => f.toFun, coe_injective' := ⋯ }
instance
CompleteLatticeHom.instCompleteLatticeHomClass
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
:
CompleteLatticeHomClass (CompleteLatticeHom α β) α β
def
CompleteLatticeHom.tosSupHom
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : CompleteLatticeHom α β)
:
sSupHom α β
Reinterpret a CompleteLatticeHom as a sSupHom.
def
CompleteLatticeHom.toBoundedLatticeHom
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : CompleteLatticeHom α β)
:
Reinterpret a CompleteLatticeHom as a BoundedLatticeHom.
Equations
- f.toBoundedLatticeHom = { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }
theorem
CompleteLatticeHom.toFun_eq_coe
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : CompleteLatticeHom α β)
:
@[simp]
theorem
CompleteLatticeHom.coe_tosInfHom
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : CompleteLatticeHom α β)
:
@[simp]
theorem
CompleteLatticeHom.coe_tosSupHom
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : CompleteLatticeHom α β)
:
@[simp]
theorem
CompleteLatticeHom.coe_toBoundedLatticeHom
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : CompleteLatticeHom α β)
:
@[simp]
theorem
CompleteLatticeHom.coe_mk
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : sInfHom α β)
(hf : ∀ (s : Set α), f.toFun (sSup s) = sSup (f.toFun '' s))
:
theorem
CompleteLatticeHom.ext
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
{f g : CompleteLatticeHom α β}
(h : ∀ (a : α), f a = g a)
:
def
CompleteLatticeHom.copy
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : CompleteLatticeHom α β)
(f' : α → β)
(h : f' = ⇑f)
:
Copy of a CompleteLatticeHom with a new toFun equal to the old one. Useful to fix
definitional equalities.
@[simp]
theorem
CompleteLatticeHom.coe_copy
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : CompleteLatticeHom α β)
(f' : α → β)
(h : f' = ⇑f)
:
theorem
CompleteLatticeHom.copy_eq
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : CompleteLatticeHom α β)
(f' : α → β)
(h : f' = ⇑f)
:
id as a CompleteLatticeHom.
Equations
- CompleteLatticeHom.id α = { toFun := id, map_sInf' := ⋯, map_sSup' := ⋯ }
instance
CompleteLatticeHom.instInhabited
(α : Type u_2)
[CompleteLattice α]
:
Inhabited (CompleteLatticeHom α α)
Equations
- CompleteLatticeHom.instInhabited α = { default := CompleteLatticeHom.id α }
@[simp]
@[simp]
def
CompleteLatticeHom.comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
(f : CompleteLatticeHom β γ)
(g : CompleteLatticeHom α β)
:
Composition of CompleteLatticeHoms as a CompleteLatticeHom.
@[simp]
theorem
CompleteLatticeHom.coe_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
(f : CompleteLatticeHom β γ)
(g : CompleteLatticeHom α β)
:
@[simp]
theorem
CompleteLatticeHom.comp_apply
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
(f : CompleteLatticeHom β γ)
(g : CompleteLatticeHom α β)
(a : α)
:
@[simp]
theorem
CompleteLatticeHom.comp_assoc
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
{δ : Type u_5}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
[CompleteLattice δ]
(f : CompleteLatticeHom γ δ)
(g : CompleteLatticeHom β γ)
(h : CompleteLatticeHom α β)
:
@[simp]
theorem
CompleteLatticeHom.comp_id
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : CompleteLatticeHom α β)
:
@[simp]
theorem
CompleteLatticeHom.id_comp
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : CompleteLatticeHom α β)
:
@[simp]
theorem
CompleteLatticeHom.cancel_right
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
{g₁ g₂ : CompleteLatticeHom β γ}
{f : CompleteLatticeHom α β}
(hf : Function.Surjective ⇑f)
:
@[simp]
theorem
CompleteLatticeHom.cancel_left
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
{g : CompleteLatticeHom β γ}
{f₁ f₂ : CompleteLatticeHom α β}
(hg : Function.Injective ⇑g)
:
Dual homs #
@[simp]
@[simp]
@[simp]
@[simp]
Reinterpret a complete lattice homomorphism as a complete lattice homomorphism between the dual lattices.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CompleteLatticeHom.dual_symm_apply_toFun
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : CompleteLatticeHom αᵒᵈ βᵒᵈ)
(a✝ : αᵒᵈᵒᵈ)
:
@[simp]
theorem
CompleteLatticeHom.dual_apply_toFun
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : CompleteLatticeHom α β)
(a✝ : αᵒᵈ)
:
@[simp]
@[simp]
theorem
CompleteLatticeHom.dual_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
(g : CompleteLatticeHom β γ)
(f : CompleteLatticeHom α β)
:
@[simp]
@[simp]
theorem
CompleteLatticeHom.symm_dual_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
(g : CompleteLatticeHom βᵒᵈ γᵒᵈ)
(f : CompleteLatticeHom αᵒᵈ βᵒᵈ)
:
Concrete homs #
def
CompleteLatticeHom.setPreimage
{α : Type u_2}
{β : Type u_3}
(f : α → β)
:
CompleteLatticeHom (Set β) (Set α)
Set.preimage as a complete lattice homomorphism.
See also sSupHom.setImage.
Equations
- CompleteLatticeHom.setPreimage f = { toFun := Set.preimage f, map_sInf' := ⋯, map_sSup' := ⋯ }
@[simp]
@[simp]
theorem
CompleteLatticeHom.setPreimage_apply
{α : Type u_2}
{β : Type u_3}
(f : α → β)
(s : Set β)
:
@[simp]
theorem
CompleteLatticeHom.setPreimage_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
(g : β → γ)
(f : α → β)
:
Using Set.image, a function between types yields a sSupHom between their lattices of
subsets.
See also CompleteLatticeHom.setPreimage.
Equations
- sSupHom.setImage f = { toFun := Set.image f, map_sSup' := ⋯ }
An equivalence of types yields an order isomorphism between their lattices of subsets.
@[simp]
@[simp]
The map (a, b) ↦ a ⊔ b as a sSupHom.
Equations
- supsSupHom = { toFun := fun (x : α × α) => x.1 ⊔ x.2, map_sSup' := ⋯ }
The map (a, b) ↦ a ⊓ b as an sInfHom.
Equations
- infsInfHom = { toFun := fun (x : α × α) => x.1 ⊓ x.2, map_sInf' := ⋯ }
@[simp]
@[simp]