upperClosure — Mathlib

English

If α is a locally finite order with a top element and s is finite, then the upper closure of s is finite.

Русский

Если α имеет локально конечный порядок с верхней границей и S конечна, то верхнее замыкание S конечна.

LaTeX

$$$ [\text{LocallyFiniteOrderTop } \alpha] \; (h s : s.Finite) : (\mathrm{upperClosure} \ s : \text{Set } \alpha).Finite $$$

Lean4

protected theorem upperClosure [LocallyFiniteOrderTop α] (hs : s.Finite) : (upperClosure s : Set α).Finite :=
  by
  rw [coe_upperClosure]
  exact hs.biUnion fun _ _ => finite_Ici _

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