Theorems · Theorem · category theory

BddDistLat.Iso.mk_inv

∀ {α β : BddDistLat} (e : ↑α.toDistLat ≃o ↑β.toDistLat),
  (BddDistLat.Iso.mk e).inv =
    BddDistLat.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.BddDistLat

Cited by

0 results in Mathlib

Foundations

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