isLowerSet_iff_forall_lt — Mathlib

English

A set is a lower set exactly when all smaller elements preserve membership: if b < a and a ∈ S, then b ∈ S.

Русский

Нижнее множество тогда и только тогда, когда для любых b < a выполнение: если a ∈ S, то b ∈ S.

LaTeX

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

Lean4

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

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