finite_range

Mathlib.MeasureTheory.Function.SimpleFunc

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

English

A simple function α →ₛ β has a finite range.

Русский

У простой функции α →ₛ β конечна область значений.

LaTeX

$$$\\text{range}(f) \\text{ is finite}$$$

Lean4

theorem finite_range (f : α →ₛ β) : (Set.range f).Finite :=
  f.finite_range'

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

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

Разделы

Аффилиация

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