comap_mono — Mathlib

English

If f is semilinear, then the image of the infimum equals the infimum of images when injectivity is assumed: map f (p ⊓ q) = map f p ⊓ map f q.

Русский

Если f полуприводимоe, и инъективность обеспечена, то образ пересечения равен пересечению образов.

LaTeX

$$(p ∩ q).map f = p.map f ∩ q.map f$$

Lean4

@[gcongr]
theorem comap_mono {f : F} {q q' : Submodule R₂ M₂} : q ≤ q' → comap f q ≤ comap f q' :=
  preimage_mono

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