Theorems · Theorem · category theory

BddLat.Iso.mk_inv

∀ {α β : BddLat} (e : ↑α.toLat ≃o ↑β.toLat),
  (BddLat.Iso.mk e).inv =
    BddLat.ofHom
      (have __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
      { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })

Defined in

Mathlib.Order.Category.BddLat

Cited by

0 results in Mathlib

Foundations

Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound