Icc_mem_vitaliFamily_at_left — Mathlib

English

Left-density statement: the left limit of Icc set around x equals a point indicator for x, as per Vitali density theorem on the real line.

Русский

Левая плотность: предел множества Icc слева от x равен индикатору точки x в пределе по теореме плотности Витали на вещественной линии.

LaTeX

$$$\forall x,\ Icc x y \text{ плотность по } x \text{ согласно Vitali.}$$$

Lean4

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

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