Icc_mem_vitaliFamily_at_right — Mathlib

English

For the Vitali cover on the real line with volume measure, the interval Icc x y is in the right set-at x whenever x<y.

Русский

Для покрытия Витали на вещественной линии с мерой объема, интервал Icc x y лежит в наборе setsAt x, если x<y.

LaTeX

$$$\forall x

Lean4

theorem Icc_mem_vitaliFamily_at_right {x y : ℝ} (hxy : x < y) :
    Icc x y ∈ (vitaliFamily (volume : Measure ℝ) 1).setsAt x :=
  by
  rw [Icc_eq_closedBall]
  refine closedBall_mem_vitaliFamily_of_dist_le_mul _ ?_ (by linarith)
  rw [dist_comm, Real.dist_eq, abs_of_nonneg] <;> linarith

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