top_notMem_iff — Mathlib

English

For any subset s of α, top ∉ s if and only if every element of s is strictly below top.

Русский

Для любого подмножества s ⊆ α верно: top ∉ s тогда и только тогда, когда каждый элемент x ∈ s удовлетворяет x < top.

LaTeX

$$$\forall s:\\mathcal{P}(\alpha),\top \notin s \iff \forall x\in s, x < \top$$$

Lean4

theorem top_notMem_iff {s : Set α} : ⊤ ∉ s ↔ ∀ x ∈ s, x < ⊤ :=
  ⟨fun h x hx ↦ Ne.lt_top (fun hx' : x = ⊤ ↦ h (hx' ▸ hx)), fun h h₀ ↦ (h ⊤ h₀).false⟩

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