Theorems · Theorem · order theory

HeytAlg.Iso.mk_inv

∀ {α β : HeytAlg} (e : ↑α ≃o ↑β),
  (HeytAlg.Iso.mk e).inv =
    HeytAlg.ofHom { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯, map_himp' := ⋯ }

Defined in

Mathlib.Order.Category.HeytAlg

Cited by

0 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Quot.sound