comap — Mathlib

English

If f x ≡ f y mod V, then x ≡ y mod V.comap f.

Русский

Если f x ≡ f y mod V, то x ≡ y mod V.comap f.

LaTeX

$$$$ V \\text{ submodule of } N,\\ f: M \\to N,\\text{ and } f x \\equiv f y\\ [SMOD\\ V] \\Rightarrow x \\equiv y\\ [SMOD\\ V.comap\\ f]. $$$$

Lean4

theorem comap {f : M →ₗ[R] N} (hxy : f x ≡ f y [SMOD V]) : x ≡ y [SMOD V.comap f] :=
  (Submodule.Quotient.eq _).2 <| show f (x - y) ∈ V from (f.map_sub x y).symm ▸ (Submodule.Quotient.eq _).1 hxy

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