Theorems · Theorem · order theory

BooleanSubalgebra.map_equiv_eq_comap_symm

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

1 results in Mathlib

Foundations

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

Assumes

BooleanAlgebraBooleanAlgebra