solidClosure_min — Mathlib

English

If s ⊆ t and t is solid, then solidClosure(s) ⊆ t. In other words, solidClosure is the least solid superset of s.

Русский

Если s ⊆ t и t солидно, то solidClosure(s) ⊆ t. Иными словами, solidClosure есть наименьшее солидное надмножество, содержащее s.

LaTeX

$$$(s \subseteq t) \to \operatorname{IsSolid}(t) \to \operatorname{solidClosure}(s) \subseteq t$$$

Lean4

theorem solidClosure_min (hst : s ⊆ t) (ht : IsSolid t) : solidClosure s ⊆ t := fun _ ⟨_, hy, hxy⟩ ↦ ht (hst hy) hxy

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