affineLocally_respectsIso — Mathlib

English

If P is invariant under isomorphisms, then the affine-locally induced property is invariant under isomorphisms.

Русский

Если P инвариантно относительно изоморфизмов, то свойство, индуцируемое локально по аффинному, также инвариантно.

LaTeX

$$$\\operatorname{RespectsIso}(P) \\Rightarrow (\\mathrm{affineLocally}\ P).\\mathrm{RespectsIso}$$$

Lean4

theorem affineLocally_respectsIso (h : RingHom.RespectsIso P) : (affineLocally P).RespectsIso :=
  letI := sourceAffineLocally_respectsIso P h
  inferInstance

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