affineLocally_le — Mathlib

English

The relation affineLocally is monotone with respect to refinement of covers.

Русский

Связь affineLocally монотонна по отношению к refinements покрытий.

LaTeX

$$affineLocally ≤ affineLocally Q$$

Lean4

theorem affineLocally_le {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) : affineLocally P ≤ affineLocally Q :=
  fun _ _ _ hf U V ↦ hPQ (hf U V)

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