eq_zero_of_mem_range_zero

Mathlib.MeasureTheory.Function.SimpleFunc

URI: https://scilib.ai/kg/mathlib#MeasureTheory.SimpleFunc.eq_zero_of_mem_range_zero

English

If 0 is in the range of a simple function, then the element is 0.

Русский

Если 0 принадлежит диапазону простой функции, то этот элемент равен нулю.

LaTeX

$$$\\forall y,\\; y \\in (0 : \\alpha \\to_{\\mathrm{S}} \\beta).range\\; \\Rightarrow\\; y = 0.$$$

Lean4

theorem eq_zero_of_mem_range_zero [Zero β] : ∀ {y : β}, y ∈ (0 : α →ₛ β).range → y = 0 :=
  @(forall_mem_range.2 fun _ => rfl)

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

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

Разделы

Аффилиация

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