negAt_apply_isReal_and_notMem — Mathlib

English

The operator negAt preserves volume for the mixed space.

Русский

Оператор negAt сохраняет объём для смешанного пространства.

LaTeX

$$volume_preserving_negAt : MeasurePreserving (negAt s)$$

Lean4

@[simp]
theorem negAt_apply_isReal_and_notMem (x : mixedSpace K) {w : { w // IsReal w }} (hw : w ∉ s) :
    (negAt s x).1 w = x.1 w := by
  simp_rw [negAt, prodCongr_apply, piCongrRight_apply, if_neg hw, ContinuousLinearEquiv.refl_apply]

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