mem_Icc

Mathlib.Geometry.Manifold.BumpFunction

URI: https://scilib.ai/kg/mathlib#SmoothBumpFunction.mem_Icc

← MathLib Explorer

English

For every x, f(x) lies in the closed interval [0,1].

Русский

Для каждого x значение f(x) принадлежит замкнутому интервалу [0,1].

LaTeX

$$$\forall x,\; f(x) \in [0,1].$$$

Lean4

theorem mem_Icc : f x ∈ Icc (0 : ℝ) 1 :=
  by
  have : f x = 0 ∨ f x = _ := indicator_eq_zero_or_self _ _ _
  rcases this with h | h <;> rw [h]
  exacts [left_mem_Icc.2 zero_le_one, ⟨f.nonneg, f.le_one⟩]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru