targetAffineLocally_affineAnd_le — Mathlib

English

If Q implies W for all R,S, then targetAffineLocally(affineAnd(Q)) ≤ targetAffineLocally(affineAnd(W)).

Русский

Если для всех R,S выполняется Q f → W f, то targetAffineLocally(affineAnd(Q)) ≤ targetAffineLocally(affineAnd(W)).

LaTeX

$$$\\operatorname{targetAffineLocally}(\\operatorname{affineAnd}(Q)) \\le \\operatorname{targetAffineLocally}(\\operatorname{affineAnd}(W))$$$

Lean4

theorem targetAffineLocally_affineAnd_le (hQW : ∀ {R S : Type u} [CommRing R] [CommRing S] {f : R →+* S}, Q f → W f) :
    targetAffineLocally (affineAnd Q) ≤ targetAffineLocally (affineAnd W) :=
  by
  intro X Y f h U
  exact ⟨(h U).1, hQW (h U).2⟩

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