Theorems · Theorem · order theory

FinBddDistLat.Iso.mk_hom

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

Defined in

Mathlib.Order.Category.FinBddDistLat

Cited by

0 results in Mathlib

Foundations

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