equivProjectivization_apply_infinity

Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

URI: https://scilib.ai/kg/mathlib#OnePoint.equivProjectivization_apply_infinity

English

Under the equivalence, the point at infinity corresponds to the projective point [1:0].

Русский

При переходе по эквивалентности бесконечность соответствует точке проективного пространства [1:0].

LaTeX

$$$\\equivProjectivization(K)(\\infty)= [1:0].$$$

Lean4

@[simp]
theorem equivProjectivization_apply_infinity : equivProjectivization K ∞ = mk K ⟨1, 0⟩ (by simp) :=
  rfl

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

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

Разделы

Аффилиация

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