isLowerSet_iff_Iio_subset — Mathlib

English

A set is a lower set exactly when it contains all smaller elements: for any a ∈ S, Iio(a) ⊆ S.

Русский

Нижнее множество содержит все меньшие элементы: для любого a ∈ S, Iio(a) ⊆ S.

LaTeX

$$IsLowerSet s ↔ ∀ ⦃a⦄, a ∈ s → Iio a ⊆ s$$

Lean4

theorem isLowerSet_iff_Iio_subset : IsLowerSet s ↔ ∀ ⦃a⦄, a ∈ s → Iio a ⊆ s := by
  simp [isLowerSet_iff_forall_lt, subset_def, @forall_swap (_ ∈ s)]

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