Theorems · Theorem · order theory

BiheytingHom.mk.inj

∀ {α : Type u_6} {β : Type u_7} {inst : BiheytingAlgebra α} {inst_1 : BiheytingAlgebra β}
  {toLatticeHom : LatticeHom α β}
  {map_himp' : ∀ (a b : α), toLatticeHom.toFun (a ⇨ b) = toLatticeHom.toFun a ⇨ toLatticeHom.toFun b}
  {map_sdiff' : ∀ (a b : α), toLatticeHom.toFun (a \ b) = toLatticeHom.toFun a \ toLatticeHom.toFun b}
  {toLatticeHom_1 : LatticeHom α β}
  {map_himp'_1 : ∀ (a b : α), toLatticeHom_1.toFun (a ⇨ b) = toLatticeHom_1.toFun a ⇨ toLatticeHom_1.toFun b}
  {map_sdiff'_1 : ∀ (a b : α), toLatticeHom_1.toFun (a \ b) = toLatticeHom_1.toFun a \ toLatticeHom_1.toFun b},
  { toLatticeHom := toLatticeHom, map_himp' := map_himp', map_sdiff' := map_sdiff' } =
      { toLatticeHom := toLatticeHom_1, map_himp' := map_himp'_1, map_sdiff' := map_sdiff'_1 } →
    toLatticeHom = toLatticeHom_1

Defined in

Mathlib.Order.Heyting.Hom

Cited by

1 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms