codRestrict_le — Mathlib

English

If A is a substructure of N, then f.codRestrict(h) ≤ f under appropriate le relations.

Русский

Если A ⊆ f.cod, то f.codRestrict(h) ≤ f, при заданных отношениях порядка.

LaTeX

$$$\forall f,g\: M \equiv_p^L N,\; \forall A\; (hf: f.cod \le A)\; (hg: A \le g.cod)\; (hfg: f \le g) \Rightarrow f \le g.\text{codRestrict}(hg).$$$

Lean4

theorem codRestrict_le (f : M ≃ₚ[L] N) {A : L.Substructure N} (h : A ≤ f.cod) : codRestrict f h ≤ f :=
  symm_le_iff.2 (f.symm.domRestrict_le h)

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