lift_mk

Mathlib.LinearAlgebra.Projectivization.Basic

URI: https://scilib.ai/kg/mathlib#Projectivization.lift_mk

← MathLib Explorer

English

The lift evaluated at the class of v equals f applied to v.

Русский

Применённый лифт к классу v равен f(v).

LaTeX

$$$ \mathrm{lift}(f, hf)(\mathrm{mk}(K,v,hv)) = f(v) $$$

Lean4

@[simp]
protected theorem lift_mk {α : Type*} (f : { v : V // v ≠ 0 } → α)
    (hf : ∀ (a b : { v : V // v ≠ 0 }) (t : K), a = t • (b : V) → f a = f b) (v : V) (hv : v ≠ 0) :
    Projectivization.lift f hf (mk K v hv) = f ⟨v, hv⟩ :=
  rfl

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

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

Разделы

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

Аффилиация

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