isUpperSet_iff_forall_lt — Mathlib

English

An upper set is exactly those sets closed under taking larger elements; equivalently, if a < b and a ∈ S then b ∈ S.

Русский

Верхнее множество состоит из элементов, замкнуто под операцией перехода к большему; если a < b и a ∈ S, то b ∈ S.

LaTeX

$$IsUpperSet s ↔ ∀ ⦃a b : α⦄, a < b → a ∈ s → b ∈ s$$

Lean4

theorem isUpperSet_iff_forall_lt : IsUpperSet s ↔ ∀ ⦃a b : α⦄, a < b → a ∈ s → b ∈ s :=
  forall_congr' fun a => by simp [le_iff_eq_or_lt, or_imp, forall_and]

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