range_snd

Mathlib.LinearAlgebra.Prod

URI: https://scilib.ai/kg/mathlib#Submodule.range_snd

English

The range of fst equals the top submodule of M ⊕ M₂, i.e. the entire first projection’s image covers all M.

Русский

Образ fst равен верхнему подмодулю M ⊕ M₂, то есть вся первая проекция достигаема.

LaTeX

$$$\\mathrm{range}(\\mathrm{fst}\\, R\\, M\\, M_2) = \\top$$$

Lean4

@[simp]
theorem range_snd : range (snd R M M₂) = ⊤ := by rw [range_eq_map, ← prod_top, prod_map_snd]

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

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

Разделы

Аффилиация

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