singleton_vsub_self — Mathlib

English

For any p ∈ P, the v-subtraction of the singleton {p} from itself equals the singleton of 0 in G: ({ p } : Set P) −ᵥ { p } = {(0 : G)}.

Русский

Для всякой точки p ∈ P операцией vsub над множеством {p} с самим собой получается множество, содержащие нуль: ({p} : Set P) −ᵥ {p} = {(0 : G)}.

LaTeX

$$$ ({p} : Set P) -ᵥ \{ p \} = { (0 : G) } $$$

Lean4

theorem singleton_vsub_self (p : P) : ({ p } : Set P) -ᵥ { p } = {(0 : G)} := by
  rw [Set.singleton_vsub_singleton, vsub_self]

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