principal_subtype — Mathlib

English

Same as above but with concrete subtype inclusion, expressing the equality of principal t and the comap of principal image under the subtype inclusion.

Русский

Аналогично: главная фильтрация t остаётся равной comap главной фильтрации образа t под включением подтипа.

LaTeX

$$$\\mathcal{P}(t) = \\mathrm{comap}(\\text{Subtype.val}) (\\mathcal{P}( (\\text{Subtype.val})'' t ))$$$

Lean4

theorem principal_subtype {α : Type*} (s : Set α) (t : Set s) : 𝓟 t = comap (↑) (𝓟 (((↑) : s → α) '' t)) := by
  rw [comap_principal, preimage_image_eq _ Subtype.coe_injective]

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