mem_of_isAtom_of_le_sSup_atoms — Mathlib

English

If a is an atom and a ≤ sSup S, then a ∈ S.

Русский

Если a атом, и a ≤ sSup S, то a ∈ S.

LaTeX

$$$ \text{IsAtom}(a) \rightarrow (a \le sSup S) \rightarrow a \in S $$$

Lean4

theorem mem_of_isAtom_of_le_sSup_atoms (hS : BooleanGenerators S) (a : α) (ha : IsAtom a) (haS : a ≤ sSup S) : a ∈ S :=
  by
  obtain ⟨T, hT, rfl⟩ := hS.atomistic a haS
  obtain rfl | ⟨a, haT⟩ := T.eq_empty_or_nonempty
  · simp only [sSup_empty] at ha
    exact (ha.1 rfl).elim
  suffices sSup T = a from this ▸ hT haT
  have : a ≤ sSup T := le_sSup haT
  rwa [ha.le_iff_eq, eq_comm] at this
  exact (hS.isAtom a (hT haT)).1

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