mem_range

Mathlib.MeasureTheory.Function.SimpleFunc

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

English

An element b belongs to the range if and only if it belongs to the underlying Finset range.

Русский

Член в диапазоне простого функция равен члену во внутреннем финитном диапазоне.

LaTeX

$$$ b \\in f.range \\;\\Leftrightarrow\\; b \\in range f $$$

Lean4

@[simp]
theorem mem_range {f : α →ₛ β} {b} : b ∈ f.range ↔ b ∈ range f :=
  Finite.mem_toFinset _

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

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

Разделы

Аффилиация

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