volume_eq_zero — Mathlib

English

If ι is finite and s ⊂ (ι → ℝ) is an antichain (no two distinct elements are comparable under coordinate-wise ≤), then the volume of s is zero.

Русский

Пусть ι конечен, и s ⊂ (ι → ℝ) является античейном (ни две различные точки не сравнимы по координатному порядку). Объём s равен нулю.

LaTeX

$$$\text{If } s \text{ is an antichain in } \mathbb{R}^{\!\iota}, \operatorname{vol}(s)=0.$$$

Lean4

theorem volume_eq_zero [Nonempty ι] (hs : IsAntichain (· ≤ ·) s) : volume s = 0 :=
  by
  refine measure_mono_null ?_ hs.ordConnected.null_frontier
  rw [← closure_diff_interior, hs.interior_eq_empty, diff_empty]
  exact subset_closure

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