English
If T1 ⊆ S and T2 ⊆ S, then sSup(T1 ∩ T2) = sSup(T1) ⊓ sSup(T2).
Русский
Если T1 ⊆ S и T2 ⊆ S, тогда sSup(T1 ∩ T2) = sSup(T1) ∧ sSup(T2).
LaTeX
$$$ \text{If } T_1 \subseteq S \text{ and } T_2 \subseteq S, \quad sSup(T_1 \cap T_2) = sSup(T_1) \wedge sSup(T_2) $$$
Lean4
theorem sSup_inter (hS : BooleanGenerators S) {T₁ T₂ : Set α} (hT₁ : T₁ ⊆ S) (hT₂ : T₂ ⊆ S) :
sSup (T₁ ∩ T₂) = (sSup T₁) ⊓ (sSup T₂) := by
apply le_antisymm
· apply le_inf
· apply sSup_le_sSup Set.inter_subset_left
· apply sSup_le_sSup Set.inter_subset_right
obtain ⟨X, hX, hX'⟩ := hS.atomistic (sSup T₁ ⊓ sSup T₂) (inf_le_left.trans (sSup_le_sSup hT₁))
rw [hX']
apply _root_.sSup_le
intro I hI
apply _root_.le_sSup
constructor
· apply (hS.mono hT₁).mem_of_isAtom_of_le_sSup_atoms _ _ _
· exact (hS.mono hX).isAtom I hI
· exact (_root_.le_sSup hI).trans (hX'.ge.trans inf_le_left)
· apply (hS.mono hT₂).mem_of_isAtom_of_le_sSup_atoms _ _ _
· exact (hS.mono hX).isAtom I hI
· exact (_root_.le_sSup hI).trans (hX'.ge.trans inf_le_right)
