negMap_eq — Mathlib

English

For any P ∈ Fin 3 → R, the negation map on the projective point represented by P corresponds to negating P itself in the underlying projective coordinates: W'.negMap ⟦P⟧ = ⟦W'.neg P⟧.

Русский

Для любого P ∈ Fin 3 → R отображение отрицания для квадрета проектной точки эквивалентно отрицанию самой точки: W'.negMap ⟦P⟧ = ⟦W'.neg P⟧.

LaTeX

$$$ W'.negMap \\llbracket P \\rrbracket = \\llbracket W'.neg P \\rrbracket $$$

Lean4

theorem negMap_eq (P : Fin 3 → R) : W'.negMap ⟦P⟧ = ⟦W'.neg P⟧ :=
  rfl

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