subtypeVal — Mathlib

English

If the defining predicate p describes a closed set, then the inclusion Subtype p → X is a closed embedding.

Русский

Если множество {a | p(a)} замкнуто, то включение Subtype p → X является замкнутым вложением.

LaTeX

$$$$ \\text{IsClosedEmbedding}(\\text{Subtype}.val) $$$$

Lean4

theorem subtypeVal (h : IsClosed {a | p a}) : IsClosedEmbedding ((↑) : Subtype p → X) :=
  ⟨.subtypeVal, by rwa [Subtype.range_coe_subtype]⟩

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