isSeparated_iso — Mathlib

English

The property of being separated is preserved by isomorphisms of presheaves: if i: P ≅ P' and P is separated for J, then P' is separated for J.

Русский

Свойство разделённости сохраняется при изоморфизме пресшефов: если P ≅ P' и P — это разделённый для J, то P' тоже разделённый для J.

LaTeX

$$$(P \cong P') \Rightarrow (\mathrm{IsSeparated}(J,P) \Rightarrow \mathrm{IsSeparated}(J,P'))$$

Lean4

/-- The property of being separated is preserved under isomorphisms. -/
theorem isSeparated_iso {P' : Cᵒᵖ ⥤ Type w} (i : P ≅ P') (hP : IsSeparated J P) : IsSeparated J P' := fun _ S hS ↦
  isSeparatedFor_iso i (hP S hS)

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