Heyting algebra morphisms #

A Heyting homomorphism between two Heyting algebras is a bounded lattice homomorphism that preserves Heyting implication.

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 #

HeytingHom: Heyting homomorphisms.
CoheytingHom: Co-Heyting homomorphisms.
BiheytingHom: Bi-Heyting homomorphisms.

Typeclasses #

source

structure HeytingHom (α : Type u_6) (β : Type u_7) [HeytingAlgebra α] [HeytingAlgebra β] extends LatticeHom :

Type (max u_6 u_7)

The type of Heyting homomorphisms from α to β. Bounded lattice homomorphisms that preserve Heyting implication.

toFun : α → β
map_sup' : ∀ (a b : α), self.toFun (a ⊔ b) = self.toFun a ⊔ self.toFun b
map_inf' : ∀ (a b : α), self.toFun (a ⊓ b) = self.toFun a ⊓ self.toFun b
map_bot' : self.toFun ⊥ = ⊥
The proposition that a Heyting homomorphism preserves the bottom element.
map_himp' : ∀ (a b : α), self.toFun (a ⇨ b) = self.toFun a ⇨ self.toFun b
The proposition that a Heyting homomorphism preserves the Heyting implication.

Instances For

source

structure CoheytingHom (α : Type u_6) (β : Type u_7) [CoheytingAlgebra α] [CoheytingAlgebra β] extends LatticeHom :

Type (max u_6 u_7)

The type of co-Heyting homomorphisms from α to β. Bounded lattice homomorphisms that preserve difference.

toFun : α → β
map_sup' : ∀ (a b : α), self.toFun (a ⊔ b) = self.toFun a ⊔ self.toFun b
map_inf' : ∀ (a b : α), self.toFun (a ⊓ b) = self.toFun a ⊓ self.toFun b
map_top' : self.toFun ⊤ = ⊤
The proposition that a co-Heyting homomorphism preserves the top element.
map_sdiff' : ∀ (a b : α), self.toFun (a \ b) = self.toFun a \ self.toFun b
The proposition that a co-Heyting homomorphism preserves the difference operation.

Instances For

source

structure BiheytingHom (α : Type u_6) (β : Type u_7) [BiheytingAlgebra α] [BiheytingAlgebra β] extends LatticeHom :

Type (max u_6 u_7)

The type of bi-Heyting homomorphisms from α to β. Bounded lattice homomorphisms that preserve Heyting implication and difference.

toFun : α → β
map_sup' : ∀ (a b : α), self.toFun (a ⊔ b) = self.toFun a ⊔ self.toFun b
map_inf' : ∀ (a b : α), self.toFun (a ⊓ b) = self.toFun a ⊓ self.toFun b
map_himp' : ∀ (a b : α), self.toFun (a ⇨ b) = self.toFun a ⇨ self.toFun b
The proposition that a bi-Heyting homomorphism preserves the Heyting implication.
map_sdiff' : ∀ (a b : α), self.toFun (a \ b) = self.toFun a \ self.toFun b
The proposition that a bi-Heyting homomorphism preserves the difference operation.

Instances For

source

class HeytingHomClass (F : Type u_6) (α : Type u_7) (β : Type u_8) [HeytingAlgebra α] [HeytingAlgebra β] [FunLike F α β] extends LatticeHomClass :

Prop

HeytingHomClass F α β states that F is a type of Heyting homomorphisms.

You should extend this class when you extend HeytingHom.

map_sup : ∀ (f : F) (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (f : F) (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : ∀ (f : F), f ⊥ = ⊥
The proposition that a Heyting homomorphism preserves the bottom element.
map_himp : ∀ (f : F) (a b : α), f (a ⇨ b) = f a ⇨ f b
The proposition that a Heyting homomorphism preserves the Heyting implication.

Instances

source

class CoheytingHomClass (F : Type u_6) (α : Type u_7) (β : Type u_8) [CoheytingAlgebra α] [CoheytingAlgebra β] [FunLike F α β] extends LatticeHomClass :

Prop

CoheytingHomClass F α β states that F is a type of co-Heyting homomorphisms.

You should extend this class when you extend CoheytingHom.

map_sup : ∀ (f : F) (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (f : F) (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : ∀ (f : F), f ⊤ = ⊤
The proposition that a co-Heyting homomorphism preserves the top element.
map_sdiff : ∀ (f : F) (a b : α), f (a \ b) = f a \ f b
The proposition that a co-Heyting homomorphism preserves the difference operation.

Instances

source

class BiheytingHomClass (F : Type u_6) (α : Type u_7) (β : Type u_8) [BiheytingAlgebra α] [BiheytingAlgebra β] [FunLike F α β] extends LatticeHomClass :

Prop

BiheytingHomClass F α β states that F is a type of bi-Heyting homomorphisms.

You should extend this class when you extend BiheytingHom.

map_sup : ∀ (f : F) (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (f : F) (a b : α), f (a ⊓ b) = f a ⊓ f b
map_himp : ∀ (f : F) (a b : α), f (a ⇨ b) = f a ⇨ f b
The proposition that a bi-Heyting homomorphism preserves the Heyting implication.
map_sdiff : ∀ (f : F) (a b : α), f (a \ b) = f a \ f b
The proposition that a bi-Heyting homomorphism preserves the difference operation.

Instances

source

instance HeytingHomClass.toBoundedLatticeHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [HeytingAlgebra α] :

∀ {x : HeytingAlgebra β} [inst : HeytingHomClass F α β], BoundedLatticeHomClass F α β

Equations

⋯ = ⋯

source

instance CoheytingHomClass.toBoundedLatticeHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [CoheytingAlgebra α] :

∀ {x : CoheytingAlgebra β} [inst : CoheytingHomClass F α β], BoundedLatticeHomClass F α β

Equations

⋯ = ⋯

source

instance BiheytingHomClass.toHeytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [BiheytingAlgebra α] :

∀ {x : BiheytingAlgebra β} [inst : BiheytingHomClass F α β], HeytingHomClass F α β

Equations

⋯ = ⋯

source

instance BiheytingHomClass.toCoheytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [BiheytingAlgebra α] :

∀ {x : BiheytingAlgebra β} [inst : BiheytingHomClass F α β], CoheytingHomClass F α β

Equations

⋯ = ⋯

source

instance OrderIsoClass.toHeytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [HeytingAlgebra α] :

∀ {x : HeytingAlgebra β} [inst : OrderIsoClass F α β], HeytingHomClass F α β

Equations

⋯ = ⋯

source

instance OrderIsoClass.toCoheytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [CoheytingAlgebra α] :

∀ {x : CoheytingAlgebra β} [inst : OrderIsoClass F α β], CoheytingHomClass F α β

Equations

⋯ = ⋯

source

instance OrderIsoClass.toBiheytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [BiheytingAlgebra α] :

∀ {x : BiheytingAlgebra β} [inst : OrderIsoClass F α β], BiheytingHomClass F α β

Equations

⋯ = ⋯

source

@[reducible]

theorem BoundedLatticeHomClass.toBiheytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [BooleanAlgebra α] [BooleanAlgebra β] [BoundedLatticeHomClass F α β] :

BiheytingHomClass F α β

This can't be an instance because of typeclass loops.

source

@[simp]

theorem map_compl {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [HeytingAlgebra α] [HeytingAlgebra β] [HeytingHomClass F α β] (f : F) (a : α) :

f aᶜ = (f a)ᶜ

source

@[simp]

theorem map_bihimp {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [HeytingAlgebra α] [HeytingAlgebra β] [HeytingHomClass F α β] (f : F) (a : α) (b : α) :

f (bihimp a b) = bihimp (f a) (f b)

source

@[simp]

theorem map_hnot {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [CoheytingAlgebra α] [CoheytingAlgebra β] [CoheytingHomClass F α β] (f : F) (a : α) :

f (￢a) = ￢f a

source

@[simp]

theorem map_symmDiff {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [CoheytingAlgebra α] [CoheytingAlgebra β] [CoheytingHomClass F α β] (f : F) (a : α) (b : α) :

f (symmDiff a b) = symmDiff (f a) (f b)

source

instance instCoeTCHeytingHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [HeytingAlgebra α] [HeytingAlgebra β] [HeytingHomClass F α β] :

CoeTC F (HeytingHom α β)

Equations

instCoeTCHeytingHom = { coe := fun (f : F) => { toLatticeHom := { toSupHom := { toFun := ⇑f, map_sup' := ⋯ }, map_inf' := ⋯ }, map_bot' := ⋯, map_himp' := ⋯ } }

source

instance instCoeTCCoheytingHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [CoheytingAlgebra α] [CoheytingAlgebra β] [CoheytingHomClass F α β] :

CoeTC F (CoheytingHom α β)

Equations

instCoeTCCoheytingHom = { coe := fun (f : F) => { toLatticeHom := { toSupHom := { toFun := ⇑f, map_sup' := ⋯ }, map_inf' := ⋯ }, map_top' := ⋯, map_sdiff' := ⋯ } }

source

instance instCoeTCBiheytingHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [BiheytingAlgebra α] [BiheytingAlgebra β] [BiheytingHomClass F α β] :

CoeTC F (BiheytingHom α β)

Equations

instCoeTCBiheytingHom = { coe := fun (f : F) => { toLatticeHom := { toSupHom := { toFun := ⇑f, map_sup' := ⋯ }, map_inf' := ⋯ }, map_himp' := ⋯, map_sdiff' := ⋯ } }

source

instance HeytingHom.instFunLike {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] :

FunLike (HeytingHom α β) α β

Equations

HeytingHom.instFunLike = { coe := fun (f : HeytingHom α β) => f.toFun, coe_injective' := ⋯ }

source

instance HeytingHom.instHeytingHomClass {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] :

HeytingHomClass (HeytingHom α β) α β

Equations

⋯ = ⋯

source

theorem HeytingHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] {f : HeytingHom α β} :

f.toFun = ⇑f

source

@[simp]

theorem HeytingHom.toFun_eq_coe_aux {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] {f : HeytingHom α β} :

⇑f.toLatticeHom = ⇑f

source

theorem HeytingHom.ext {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] {f : HeytingHom α β} {g : HeytingHom α β} (h : ∀ (a : α), f a = g a) :

f = g

source

def HeytingHom.copy {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] (f : HeytingHom α β) (f' : α → β) (h : f' = ⇑f) :

HeytingHom α β

Copy of a HeytingHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations

HeytingHom.copy f f' h = { toLatticeHom := { toSupHom := { toFun := f', map_sup' := ⋯ }, map_inf' := ⋯ }, map_bot' := ⋯, map_himp' := ⋯ }

Instances For

source

@[simp]

theorem HeytingHom.coe_copy {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] (f : HeytingHom α β) (f' : α → β) (h : f' = ⇑f) :

⇑(HeytingHom.copy f f' h) = f'

source

theorem HeytingHom.copy_eq {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] (f : HeytingHom α β) (f' : α → β) (h : f' = ⇑f) :

HeytingHom.copy f f' h = f

source

def HeytingHom.id (α : Type u_2) [HeytingAlgebra α] :

HeytingHom α α

id as a HeytingHom.

Equations

HeytingHom.id α = let __src := BotHom.id α; { toLatticeHom := LatticeHom.id α, map_bot' := ⋯, map_himp' := ⋯ }

Instances For

source

@[simp]

theorem HeytingHom.coe_id (α : Type u_2) [HeytingAlgebra α] :

⇑(HeytingHom.id α) = id

source

@[simp]

theorem HeytingHom.id_apply {α : Type u_2} [HeytingAlgebra α] (a : α) :

(HeytingHom.id α) a = a

source

instance HeytingHom.instInhabitedHeytingHom {α : Type u_2} [HeytingAlgebra α] :

Inhabited (HeytingHom α α)

Equations

HeytingHom.instInhabitedHeytingHom = { default := HeytingHom.id α }

source

instance HeytingHom.instPartialOrderHeytingHom {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] :

PartialOrder (HeytingHom α β)

Equations

HeytingHom.instPartialOrderHeytingHom = PartialOrder.lift (fun (f : HeytingHom α β) => ⇑f) ⋯

source

def HeytingHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [HeytingAlgebra α] [HeytingAlgebra β] [HeytingAlgebra γ] (f : HeytingHom β γ) (g : HeytingHom α β) :

HeytingHom α γ

Composition of HeytingHoms as a HeytingHom.

Equations

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

Instances For

source

@[simp]

theorem HeytingHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [HeytingAlgebra α] [HeytingAlgebra β] [HeytingAlgebra γ] (f : HeytingHom β γ) (g : HeytingHom α β) :

⇑(HeytingHom.comp f g) = ⇑f ∘ ⇑g

source

@[simp]

theorem HeytingHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [HeytingAlgebra α] [HeytingAlgebra β] [HeytingAlgebra γ] (f : HeytingHom β γ) (g : HeytingHom α β) (a : α) :

(HeytingHom.comp f g) a = f (g a)

source

@[simp]

theorem HeytingHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [HeytingAlgebra α] [HeytingAlgebra β] [HeytingAlgebra γ] [HeytingAlgebra δ] (f : HeytingHom γ δ) (g : HeytingHom β γ) (h : HeytingHom α β) :

HeytingHom.comp (HeytingHom.comp f g) h = HeytingHom.comp f (HeytingHom.comp g h)

source

@[simp]

theorem HeytingHom.comp_id {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] (f : HeytingHom α β) :

HeytingHom.comp f (HeytingHom.id α) = f

source

@[simp]

theorem HeytingHom.id_comp {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] (f : HeytingHom α β) :

HeytingHom.comp (HeytingHom.id β) f = f

source

@[simp]

theorem HeytingHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [HeytingAlgebra α] [HeytingAlgebra β] [HeytingAlgebra γ] {f : HeytingHom α β} {g₁ : HeytingHom β γ} {g₂ : HeytingHom β γ} (hf : Function.Surjective ⇑f) :

HeytingHom.comp g₁ f = HeytingHom.comp g₂ f ↔ g₁ = g₂

source

@[simp]

theorem HeytingHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [HeytingAlgebra α] [HeytingAlgebra β] [HeytingAlgebra γ] {f₁ : HeytingHom α β} {f₂ : HeytingHom α β} {g : HeytingHom β γ} (hg : Function.Injective ⇑g) :

HeytingHom.comp g f₁ = HeytingHom.comp g f₂ ↔ f₁ = f₂

source

instance CoheytingHom.instFunLikeCoheytingHom {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] :

FunLike (CoheytingHom α β) α β

Equations

CoheytingHom.instFunLikeCoheytingHom = { coe := fun (f : CoheytingHom α β) => f.toFun, coe_injective' := ⋯ }

source

instance CoheytingHom.instCoheytingHomClassCoheytingHomInstFunLikeCoheytingHom {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] :

CoheytingHomClass (CoheytingHom α β) α β

Equations

⋯ = ⋯

source

theorem CoheytingHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] {f : CoheytingHom α β} :

f.toFun = ⇑f

source

@[simp]

theorem CoheytingHom.toFun_eq_coe_aux {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] {f : CoheytingHom α β} :

⇑f.toLatticeHom = ⇑f

source

theorem CoheytingHom.ext {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] {f : CoheytingHom α β} {g : CoheytingHom α β} (h : ∀ (a : α), f a = g a) :

f = g

source

def CoheytingHom.copy {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] (f : CoheytingHom α β) (f' : α → β) (h : f' = ⇑f) :

CoheytingHom α β

Copy of a CoheytingHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations

CoheytingHom.copy f f' h = { toLatticeHom := { toSupHom := { toFun := f', map_sup' := ⋯ }, map_inf' := ⋯ }, map_top' := ⋯, map_sdiff' := ⋯ }

Instances For

source

@[simp]

theorem CoheytingHom.coe_copy {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] (f : CoheytingHom α β) (f' : α → β) (h : f' = ⇑f) :

⇑(CoheytingHom.copy f f' h) = f'

source

theorem CoheytingHom.copy_eq {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] (f : CoheytingHom α β) (f' : α → β) (h : f' = ⇑f) :

CoheytingHom.copy f f' h = f

source

def CoheytingHom.id (α : Type u_2) [CoheytingAlgebra α] :

CoheytingHom α α

id as a CoheytingHom.

Equations

CoheytingHom.id α = let __src := TopHom.id α; { toLatticeHom := LatticeHom.id α, map_top' := ⋯, map_sdiff' := ⋯ }

Instances For

source

@[simp]

theorem CoheytingHom.coe_id (α : Type u_2) [CoheytingAlgebra α] :

⇑(CoheytingHom.id α) = id

source

@[simp]

theorem CoheytingHom.id_apply {α : Type u_2} [CoheytingAlgebra α] (a : α) :

(CoheytingHom.id α) a = a

source

instance CoheytingHom.instInhabitedCoheytingHom {α : Type u_2} [CoheytingAlgebra α] :

Inhabited (CoheytingHom α α)

Equations

CoheytingHom.instInhabitedCoheytingHom = { default := CoheytingHom.id α }

source

instance CoheytingHom.instPartialOrderCoheytingHom {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] :

PartialOrder (CoheytingHom α β)

Equations

CoheytingHom.instPartialOrderCoheytingHom = PartialOrder.lift (fun (f : CoheytingHom α β) => ⇑f) ⋯

source

def CoheytingHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CoheytingAlgebra α] [CoheytingAlgebra β] [CoheytingAlgebra γ] (f : CoheytingHom β γ) (g : CoheytingHom α β) :

CoheytingHom α γ

Composition of CoheytingHoms as a CoheytingHom.

Equations

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

Instances For

source

@[simp]

theorem CoheytingHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CoheytingAlgebra α] [CoheytingAlgebra β] [CoheytingAlgebra γ] (f : CoheytingHom β γ) (g : CoheytingHom α β) :

⇑(CoheytingHom.comp f g) = ⇑f ∘ ⇑g

source

@[simp]

theorem CoheytingHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CoheytingAlgebra α] [CoheytingAlgebra β] [CoheytingAlgebra γ] (f : CoheytingHom β γ) (g : CoheytingHom α β) (a : α) :

(CoheytingHom.comp f g) a = f (g a)

source

@[simp]

theorem CoheytingHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [CoheytingAlgebra α] [CoheytingAlgebra β] [CoheytingAlgebra γ] [CoheytingAlgebra δ] (f : CoheytingHom γ δ) (g : CoheytingHom β γ) (h : CoheytingHom α β) :

CoheytingHom.comp (CoheytingHom.comp f g) h = CoheytingHom.comp f (CoheytingHom.comp g h)

source

@[simp]

theorem CoheytingHom.comp_id {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] (f : CoheytingHom α β) :

CoheytingHom.comp f (CoheytingHom.id α) = f

source

@[simp]

theorem CoheytingHom.id_comp {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] (f : CoheytingHom α β) :

CoheytingHom.comp (CoheytingHom.id β) f = f

source

@[simp]

theorem CoheytingHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CoheytingAlgebra α] [CoheytingAlgebra β] [CoheytingAlgebra γ] {f : CoheytingHom α β} {g₁ : CoheytingHom β γ} {g₂ : CoheytingHom β γ} (hf : Function.Surjective ⇑f) :

CoheytingHom.comp g₁ f = CoheytingHom.comp g₂ f ↔ g₁ = g₂

source

@[simp]

theorem CoheytingHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CoheytingAlgebra α] [CoheytingAlgebra β] [CoheytingAlgebra γ] {f₁ : CoheytingHom α β} {f₂ : CoheytingHom α β} {g : CoheytingHom β γ} (hg : Function.Injective ⇑g) :

CoheytingHom.comp g f₁ = CoheytingHom.comp g f₂ ↔ f₁ = f₂

source

instance BiheytingHom.instFunLikeBiheytingHom {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] :

FunLike (BiheytingHom α β) α β

Equations

BiheytingHom.instFunLikeBiheytingHom = { coe := fun (f : BiheytingHom α β) => f.toFun, coe_injective' := ⋯ }

source

instance BiheytingHom.instBiheytingHomClassBiheytingHomInstFunLikeBiheytingHom {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] :

BiheytingHomClass (BiheytingHom α β) α β

Equations

⋯ = ⋯

source

theorem BiheytingHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] {f : BiheytingHom α β} :

f.toFun = ⇑f

source

@[simp]

theorem BiheytingHom.toFun_eq_coe_aux {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] {f : BiheytingHom α β} :

⇑f.toLatticeHom = ⇑f

source

theorem BiheytingHom.ext {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] {f : BiheytingHom α β} {g : BiheytingHom α β} (h : ∀ (a : α), f a = g a) :

f = g

source

def BiheytingHom.copy {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] (f : BiheytingHom α β) (f' : α → β) (h : f' = ⇑f) :

BiheytingHom α β

Copy of a BiheytingHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations

BiheytingHom.copy f f' h = { toLatticeHom := { toSupHom := { toFun := f', map_sup' := ⋯ }, map_inf' := ⋯ }, map_himp' := ⋯, map_sdiff' := ⋯ }

Instances For

source

@[simp]

theorem BiheytingHom.coe_copy {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] (f : BiheytingHom α β) (f' : α → β) (h : f' = ⇑f) :

⇑(BiheytingHom.copy f f' h) = f'

source

theorem BiheytingHom.copy_eq {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] (f : BiheytingHom α β) (f' : α → β) (h : f' = ⇑f) :

BiheytingHom.copy f f' h = f

source

def BiheytingHom.id (α : Type u_2) [BiheytingAlgebra α] :

BiheytingHom α α

id as a BiheytingHom.

Equations

BiheytingHom.id α = let __src := HeytingHom.id α; let __src := CoheytingHom.id α; { toLatticeHom := LatticeHom.id α, map_himp' := ⋯, map_sdiff' := ⋯ }

Instances For

source

@[simp]

theorem BiheytingHom.coe_id (α : Type u_2) [BiheytingAlgebra α] :

⇑(BiheytingHom.id α) = id

source

@[simp]

theorem BiheytingHom.id_apply {α : Type u_2} [BiheytingAlgebra α] (a : α) :

(BiheytingHom.id α) a = a

source

instance BiheytingHom.instInhabitedBiheytingHom {α : Type u_2} [BiheytingAlgebra α] :

Inhabited (BiheytingHom α α)

Equations

BiheytingHom.instInhabitedBiheytingHom = { default := BiheytingHom.id α }

source

instance BiheytingHom.instPartialOrderBiheytingHom {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] :

PartialOrder (BiheytingHom α β)

Equations

BiheytingHom.instPartialOrderBiheytingHom = PartialOrder.lift (fun (f : BiheytingHom α β) => ⇑f) ⋯

source

def BiheytingHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [BiheytingAlgebra α] [BiheytingAlgebra β] [BiheytingAlgebra γ] (f : BiheytingHom β γ) (g : BiheytingHom α β) :

BiheytingHom α γ

Composition of BiheytingHoms as a BiheytingHom.

Equations

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

Instances For

source

@[simp]

theorem BiheytingHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [BiheytingAlgebra α] [BiheytingAlgebra β] [BiheytingAlgebra γ] (f : BiheytingHom β γ) (g : BiheytingHom α β) :

⇑(BiheytingHom.comp f g) = ⇑f ∘ ⇑g

source

@[simp]

theorem BiheytingHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [BiheytingAlgebra α] [BiheytingAlgebra β] [BiheytingAlgebra γ] (f : BiheytingHom β γ) (g : BiheytingHom α β) (a : α) :

(BiheytingHom.comp f g) a = f (g a)

source

@[simp]

theorem BiheytingHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [BiheytingAlgebra α] [BiheytingAlgebra β] [BiheytingAlgebra γ] [BiheytingAlgebra δ] (f : BiheytingHom γ δ) (g : BiheytingHom β γ) (h : BiheytingHom α β) :

BiheytingHom.comp (BiheytingHom.comp f g) h = BiheytingHom.comp f (BiheytingHom.comp g h)

source

@[simp]

theorem BiheytingHom.comp_id {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] (f : BiheytingHom α β) :

BiheytingHom.comp f (BiheytingHom.id α) = f

source

@[simp]

theorem BiheytingHom.id_comp {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] (f : BiheytingHom α β) :

BiheytingHom.comp (BiheytingHom.id β) f = f

source

@[simp]

theorem BiheytingHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [BiheytingAlgebra α] [BiheytingAlgebra β] [BiheytingAlgebra γ] {f : BiheytingHom α β} {g₁ : BiheytingHom β γ} {g₂ : BiheytingHom β γ} (hf : Function.Surjective ⇑f) :

BiheytingHom.comp g₁ f = BiheytingHom.comp g₂ f ↔ g₁ = g₂

source

@[simp]

theorem BiheytingHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [BiheytingAlgebra α] [BiheytingAlgebra β] [BiheytingAlgebra γ] {f₁ : BiheytingHom α β} {f₂ : BiheytingHom α β} {g : BiheytingHom β γ} (hg : Function.Injective ⇑g) :

BiheytingHom.comp g f₁ = BiheytingHom.comp g f₂ ↔ f₁ = f₂

Documentation

Mathlib.Order.Heyting.Hom

Heyting algebra morphisms #

Types of morphisms #

Typeclasses #