Theorems · Theorem · order theory

HeytingHom.mk.inj

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

Defined in

Mathlib.Order.Heyting.Hom

Cited by

1 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms