lowerClosure — Mathlib

English

In a locally finite order with a bottom element, the lower closure of a finite set is finite.

Русский

В локально конечном порядке с нулём нижнее замыкание конечного множества конечна.

LaTeX

$$$s \text{finite} \implies (\operatorname{LowerClosure}(s)\text{ finite}).$$$

Lean4

protected theorem lowerClosure [LocallyFiniteOrderBot α] (hs : s.Finite) : (lowerClosure s : Set α).Finite :=
  by
  rw [coe_lowerClosure]
  exact hs.biUnion fun _ _ => finite_Iic _

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