Theorems · Theorem · order theory

BooleanSubalgebra.comap_equiv_eq_map_symm

∀ {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β] (f : β ≃o α)
  (L : BooleanSubalgebra α),
  BooleanSubalgebra.comap
      (let __src := { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ };
      { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
      L =
    BooleanSubalgebra.map
      (let __src := { toFun := ⇑f.symm, map_sup' := ⋯, map_inf' := ⋯ };
      { toFun := ⇑f.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
      L

Defined in

Mathlib.Order.BooleanSubalgebra

Cited by

0 results in Mathlib

Foundations

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

Assumes

BooleanAlgebraBooleanAlgebra