fixedPoints_subset_range

Mathlib.Dynamics.FixedPoints.Basic

URI: https://scilib.ai/kg/mathlib#Function.fixedPoints_subset_range

English

The set of fixed points of the identity map is the entire space.

Русский

Множество фикcированных точек тождественной отображения равно всей области определения.

LaTeX

$$$fixedPoints(id) = Set.univ$$$

Lean4

theorem fixedPoints_subset_range : fixedPoints f ⊆ Set.range f := fun x hx => ⟨x, hx⟩

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

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

Разделы

Аффилиация

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