volume_eq_zero — Mathlib

English

For a fixed place w, the set { x in realSpace(K) | x(w) = 0 } has volume zero.

Русский

Для фиксированного места w множество { x в realSpace(K) | x(w) = 0 } имеет нулевой объем.

LaTeX

$$volume({x ∈ realSpace(K) : x(w) = 0}) = 0$$

Lean4

/-- The set of points in the `realSpace` that are equal to `0` at a fixed place has volume zero. -/
theorem volume_eq_zero [NumberField K] (w : InfinitePlace K) : volume ({x : realSpace K | x w = 0}) = 0 :=
  by
  let A : AffineSubspace ℝ (realSpace K) :=
    Submodule.toAffineSubspace (Submodule.mk ⟨⟨{x | x w = 0}, by simp_all⟩, rfl⟩ (by simp_all))
  convert Measure.addHaar_affineSubspace volume A fun h ↦ ?_
  simpa [A] using (h ▸ Set.mem_univ _ : 1 ∈ A)

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