indicator_le_apprSeq — Mathlib

English

For every n, the indicator of F is bounded above by hF.apprSeq n.

Русский

Для каждого n индикатор F не превосходит hF.apprSeq n.

LaTeX

$$$\\forall X \\; [TopologicalSpace X] \\; [HasOuterApproxClosed X] \\; {F : Set X} \\; (hF : IsClosed F) \\Rightarrow \\text{apprSeq } n x \\ge \\mathbf{1}_F(x) \\text{ for all } x$$

Lean4

theorem indicator_le_apprSeq (n : ℕ) : indicator F (fun _ ↦ 1) ≤ hF.apprSeq n :=
  by
  intro x
  by_cases hxF : x ∈ F
  · simp only [hxF, indicator_of_mem, apprSeq_apply_eq_one hF n, le_refl]
  · simp only [hxF, not_false_eq_true, indicator_of_notMem, zero_le]

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