Theorems · Theorem · order theory

IsCompactlyGenerated.BooleanGenerators.sSup_inter

∀ {α : Type u_1} [inst : CompleteLattice α] {S : Set α} [IsCompactlyGenerated α],
  IsCompactlyGenerated.BooleanGenerators S → ∀ {T₁ T₂ : Set α}, T₁ ⊆ S → T₂ ⊆ S → sSup (T₁ ∩ T₂) = sSup T₁ ⊓ sSup T₂

Defined in

Mathlib.Order.BooleanGenerators

Cited by

0 results in Mathlib

Foundations

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

Assumes

CompleteLatticeIsCompactlyGenerated