map₂_bot_left

Mathlib.Algebra.Module.Submodule.Bilinear

URI: https://scilib.ai/kg/mathlib#Submodule.map₂_bot_left

← MathLib Explorer

English

Again, map₂ f ⊥ q = ⊥.

Русский

Снова map₂ f ⊥ q = ⊥.

LaTeX

$$map₂ f ⊥ q = ⊥$$

Lean4

@[simp]
theorem map₂_bot_left (f : M →ₗ[R] N →ₗ[R] P) (q : Submodule R N) : map₂ f ⊥ q = ⊥ :=
  eq_bot_iff.2 <|
    map₂_le.2 fun m hm n _ => by
      rw [Submodule.mem_bot] at hm ⊢
      rw [hm, LinearMap.map_zero₂]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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