Theorems · Theorem · order theory

BooleanSubalgebra.mk.inj

∀ {α : Type u_2} {inst : BooleanAlgebra α} {toSublattice : Sublattice α}
  {compl_mem' : ∀ {a : α}, a ∈ toSublattice.carrier → aᶜ ∈ toSublattice.carrier} {bot_mem' : ⊥ ∈ toSublattice.carrier}
  {toSublattice_1 : Sublattice α} {compl_mem'_1 : ∀ {a : α}, a ∈ toSublattice_1.carrier → aᶜ ∈ toSublattice_1.carrier}
  {bot_mem'_1 : ⊥ ∈ toSublattice_1.carrier},
  { toSublattice := toSublattice, compl_mem' := compl_mem', bot_mem' := bot_mem' } =
      { toSublattice := toSublattice_1, compl_mem' := compl_mem'_1, bot_mem' := bot_mem'_1 } →
    toSublattice = toSublattice_1

Defined in

Mathlib.Order.BooleanSubalgebra

Cited by

1 results in Mathlib

Foundations

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