top_mem — Mathlib

English

In an order with a top element, a lower set contains the top element if and only if it is nonempty.

Русский

В порядке с верхней границей элемент верхний принадлежит нижнему множеству тогда и только тогда, когда множество непусто.

LaTeX

$$top_mem (hs : IsLowerSet s) : ⊤ ∈ s ↔ s.Nonempty$$

Lean4

theorem top_mem (hs : IsLowerSet s) : ⊤ ∈ s ↔ s = univ :=
  ⟨fun h => eq_univ_of_forall fun _ => hs le_top h, fun h => h.symm ▸ mem_univ _⟩

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