Theorems · Theorem · order theory

FinBoolAlg.Iso.mk_inv

∀ {α β : FinBoolAlg} (e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg),
  (FinBoolAlg.Iso.mk e).inv =
    CategoryTheory.InducedCategory.homMk
      (BoolAlg.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.FinBoolAlg

Cited by

0 results in Mathlib

Foundations

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