comap_top

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

URI: https://scilib.ai/kg/mathlib#AffineSubspace.comap_top

← MathLib Explorer

English

The comap of the top subspace is the top subspace.

Русский

Обратное образ верхнего подпространства есть верхнее подпространство.

LaTeX

$$$ (\\\\top : \\mathrm{AffineSubspace}_k P_2).comap f = \\\\top $$$

Lean4

@[simp]
theorem comap_top {f : P₁ →ᵃ[k] P₂} : (⊤ : AffineSubspace k P₂).comap f = ⊤ :=
  by
  rw [AffineSubspace.ext_iff]
  exact preimage_univ (f := f)

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

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

Разделы

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

Аффилиация

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