forallLTEqZero_supp_BddBelow — Mathlib

English

If f vanishes below n, then the support of f is bounded below.

Русский

Если f обращает ноль ниже n, то опора функции f ограничена снизу.

LaTeX

$$BddBelow (Function.support f)$$

Lean4

theorem forallLTEqZero_supp_BddBelow (f : Γ → R) (n : Γ) (hn : ∀ (m : Γ), m < n → f m = 0) :
    BddBelow (Function.support f) :=
  by
  simp only [BddBelow, Set.Nonempty, lowerBounds]
  use n
  intro m hm
  rw [Function.mem_support, ne_eq] at hm
  exact not_lt.mp (mt (hn m) hm)

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