eqOn_refl

Mathlib.Data.Set.Function

URI: https://scilib.ai/kg/mathlib#Set.eqOn_refl

English

EqOn f f s holds for any f and s.

Русский

EqOn f f s выполняется для любых f и s.

LaTeX

$$$ \forall f : \alpha \to \beta, \forall s, \mathrm{EqOn}\, f f s$$$

Lean4

theorem eqOn_refl (f : α → β) (s : Set α) : EqOn f f s := fun _ _ => rfl

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

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

Разделы

Аффилиация

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