sSup_le_sSup_iff_of_atoms — Mathlib

English

For X,Y ⊆ S, sSup X ≤ sSup Y if and only if X ⊆ Y.

Русский

Для X,Y ⊆ S верно sSup X ≤ sSup Y тогда и только тогда, когда X ⊆ Y.

LaTeX

$$$ \text{IsCompactlyGenerated.BooleanGenerators } S \rightarrow (X \subseteq S) \rightarrow (Y \subseteq S) \rightarrow \bigl( sSup X \le sSup Y \iff X \subseteq Y \bigr) $$$

Lean4

theorem sSup_le_sSup_iff_of_atoms (hS : BooleanGenerators S) (X Y : Set α) (hX : X ⊆ S) (hY : Y ⊆ S) :
    sSup X ≤ sSup Y ↔ X ⊆ Y := by
  refine ⟨?_, sSup_le_sSup⟩
  intro h a ha
  apply (hS.mono hY).mem_of_isAtom_of_le_sSup_atoms _ _ ((le_sSup ha).trans h)
  exact (hS.mono hX).isAtom a ha

Похожие утверждения