locally_of_locally — Mathlib

English

If P implies Q under isomorphisms, then Locally P implies Locally Q.

Русский

Если P под издательством изоморфизмов имплицирует Q, то Locally P влечет Locally Q.

LaTeX

$$$\text{If }\text{RespectsIso}(P)\text{ and }P\Rightarrow Q,\ \text{then }\text{Locally }P f\Rightarrow \text{Locally }Q f.$$$

Lean4

theorem locally_of_locally {Q : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop}
    (hPQ : ∀ {R S : Type u} [CommRing R] [CommRing S] {f : R →+* S}, P f → Q f) {R S : Type u} [CommRing R] [CommRing S]
    {f : R →+* S} (hf : Locally P f) : Locally Q f :=
  by
  obtain ⟨s, hsone, hs⟩ := hf
  exact ⟨s, hsone, fun t ht ↦ hPQ (hs t ht)⟩

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