le_codRestrict — Mathlib

English

Monotonicity of codomain restriction for partial equivalences: if f ≤ g, then f.codRestrict ≤ g.codRestrict under appropriate bounds.

Русский

Монотонность ограничения кода для частичных эквивалентностей: если f ≤ g, тогда f.codRestrict ≤ g.codRestrict под подходящими ограничениями.

LaTeX

$$$$ \\forall f,g \\; (f \\le g) \\Rightarrow (f.codRestrict \\le g.codRestrict). $$$$

Lean4

theorem le_codRestrict (f g : M ≃ₚ[L] N) {A : L.Substructure N} (hf : f.cod ≤ A) (hg : A ≤ g.cod) (hfg : f ≤ g) :
    f ≤ g.codRestrict hg :=
  symm_le_iff.1 (le_domRestrict f.symm g.symm hf hg (monotone_symm hfg))

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