inf_comap_le_comap_add — Mathlib

English

For linear maps f1, f2 and a submodule q, the infimum of comaps satisfies comap f1 q ⊓ comap f2 q ≤ comap (f1 + f2) q.

Русский

Для линейных отображений f1, f2 и подмодуля q справедливо: infimum(comap f1 q, comap f2 q) ≤ comap (f1+f2) q.

LaTeX

$$$ comap f_1 q \\;\\sqcap\\; comap f_2 q \\leq comap (f_1 + f_2) q $$$

Lean4

theorem inf_comap_le_comap_add (f₁ f₂ : M →ₛₗ[τ₁₂] M₂) : comap f₁ q ⊓ comap f₂ q ≤ comap (f₁ + f₂) q :=
  by
  rw [SetLike.le_def]
  intro m h
  change f₁ m + f₂ m ∈ q
  change f₁ m ∈ q ∧ f₂ m ∈ q at h
  apply q.add_mem h.1 h.2

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