chainClosure_empty — Mathlib

English

ChainClosure r of the empty set is nontrivial; in fact the empty set is a chain closure under r.

Русский

ChainClosure r для пустого множества является тривиальным; пустое множество образует цепь.

LaTeX

$$$ ChainClosure\, r\, \emptyset $$$

Lean4

theorem chainClosure_empty : ChainClosure r ∅ :=
  by
  have : ChainClosure r (⋃₀ ∅) := ChainClosure.union fun a h => (notMem_empty _ h).elim
  simpa using this

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