mulMap_range — Mathlib

English

As above, the image of mulMap is the join of A and B.

Русский

Как выше, образ mulMap есть объединение A и B.

LaTeX

$$$\operatorname{range}(A.mulMap B) = A \sqcup B$$$

Lean4

theorem mulMap_range : LinearMap.range (mulMap M N) = M * N :=
  by
  refine le_antisymm ?_ (mul_le.2 fun m hm n hn ↦ ⟨⟨m, hm⟩ ⊗ₜ[R] ⟨n, hn⟩, rfl⟩)
  rintro _ ⟨x, rfl⟩
  induction x with
  | zero => rw [map_zero]; exact zero_mem _
  | tmul a b => exact mul_mem_mul a.2 b.2
  | add a b ha hb => rw [map_add]; exact add_mem ha hb

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