Ici — Mathlib

English

For any a in α, Ici(a) is the principal upper set generated by a, i.e., {x ∈ α | a ≤ x}.

Русский

Для любого a в α существует принципиальное верхнее множество Ici(a), порождаемое a, то есть {x ∈ α | a ≤ x}.

LaTeX

$$$ \text{Ici}(a) = \{ x \in \alpha \mid a \le x \} $$$

Lean4

/-- Principal upper set. `Set.Ici` as an upper set. The smallest upper set containing a given
element. -/
nonrec def Ici (a : α) : UpperSet α :=
  ⟨Ici a, isUpperSet_Ici a⟩

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