disjoint_inl_inr

Mathlib.LinearAlgebra.Prod

URI: https://scilib.ai/kg/mathlib#LinearMap.disjoint_inl_inr

English

The ranges of inl and inr are disjoint; only the zero element lies in both.

Русский

Образы inl и inr не пересекаются кроме нуля; пересечение равно {0}.

LaTeX

$$$ Disjoint(\\text{range}(\\text{inl } R M M_2), \\text{range}(\\text{inr } R M M_2)) $$$

Lean4

theorem disjoint_inl_inr : Disjoint (range <| inl R M M₂) (range <| inr R M M₂) := by
  simp +contextual [disjoint_def, @eq_comm M 0]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru