isSolid_solidClosure — Mathlib

English

For any subset s of α, the solid closure of s is a solid set; i.e., if x ∈ solidClosure(s) and |y| ≤ |x|, then y ∈ solidClosure(s).

Русский

Для любого подмножества s в α его солидное замыкание является солидным множеством; т.е. если x ∈ solidClosure(s) и |y| ≤ |x|, то y ∈ solidClosure(s).

LaTeX

$$$\operatorname{IsSolid}(\operatorname{solidClosure}(s))$$$

Lean4

theorem isSolid_solidClosure (s : Set α) : IsSolid (solidClosure s) := fun _ ⟨y, hy, hxy⟩ _ hzx ↦ ⟨y, hy, hzx.trans hxy⟩

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