eqOn_empty

Mathlib.Data.Set.Function

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

English

EqOn f1 f2 on the empty set holds trivially.

Русский

EqOn f1 f2 на пустом множестве тривиально выполняется.

LaTeX

$$$ \forall {f_1 f_2 : \alpha \to \beta}, \mathrm{EqOn}\, f_1 f_2 \emptyset$$

Lean4

@[simp]
theorem eqOn_empty (f₁ f₂ : α → β) : EqOn f₁ f₂ ∅ := fun _ => False.elim

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

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

Разделы

Аффилиация

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