toSet_range

Mathlib.SetTheory.ZFC.Basic

URI: https://scilib.ai/kg/mathlib#ZFSet.toSet_range

English

toSet(image f x) = f'' x.toSet.

Русский

toSet образа f на x равен образу функции f над множеством x.

LaTeX

$$$(\\mathrm{image}\\ f\\ x)^{\\text{toSet}} = f''\\ x^{\\text{toSet}}$$$

Lean4

@[simp]
theorem toSet_range {α} [Small.{u} α] (f : α → ZFSet.{u}) : (range f).toSet = Set.range f :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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