negMap_eq — Mathlib

English

The negMap operation commutes with taking the quotient class: negMap ⟦P⟧ equals ⟦W'.neg P⟧.

Русский

Операция negMap сохраняет эквивалентность при взятии классa по нормируемой тождественности: 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

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