isUpperSet_iff_Ioi_subset — Mathlib

English

An upper set is exactly those sets containing all strictly larger elements; equivalently, if a ∈ S then Ioi(a) ⊆ S.

Русский

Верхнее множество содержит все элементы, большие заданного; эквивалентно: если a ∈ S, то Ioi(a) ⊆ S.

LaTeX

$$IsUpperSet s ↔ ∀ ⦃a⦄, a ∈ s → Ioi a ⊆ s$$

Lean4

theorem isUpperSet_iff_Ioi_subset : IsUpperSet s ↔ ∀ ⦃a⦄, a ∈ s → Ioi a ⊆ s := by
  simp [isUpperSet_iff_forall_lt, subset_def, @forall_swap (_ ∈ s)]

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