Theorems · Definition · order theory

CoheytingHom.mk.noConfusion

{α : Type u_6} →
  {β : Type u_7} →
    {inst : CoheytingAlgebra α} →
      {inst_1 : CoheytingAlgebra β} →
        {P : Sort u} →
          {toLatticeHom : LatticeHom α β} →
            {map_top' : toLatticeHom.toFun ⊤ = ⊤} →
              {map_sdiff' : ∀ (a b : α), toLatticeHom.toFun (a \ b) = toLatticeHom.toFun a \ toLatticeHom.toFun b} →
                {toLatticeHom' : LatticeHom α β} →
                  {map_top'' : toLatticeHom'.toFun ⊤ = ⊤} →
                    {map_sdiff'' :
                        ∀ (a b : α), toLatticeHom'.toFun (a \ b) = toLatticeHom'.toFun a \ toLatticeHom'.toFun b} →
                      { toLatticeHom := toLatticeHom, map_top' := map_top', map_sdiff' := map_sdiff' } =
                          { toLatticeHom := toLatticeHom', map_top' := map_top'', map_sdiff' := map_sdiff'' } →
                        (toLatticeHom ≍ toLatticeHom' → P) → P

Defined in

Mathlib.Order.Heyting.Hom

Cited by

1 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms