eqOn_union

Mathlib.Data.Set.Function

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

English

EqOn on a union equals conjunction of EqOn on each piece.

Русский

EqOn на объединении равно логическому conjunctionEqOn по частям.

LaTeX

$$$ \mathrm{EqOn}\, f_1 f_2 (s_1 \cup s_2) \iff \mathrm{EqOn}\, f_1 f_2 s_1 \land \mathrm{EqOn}\, f_1 f_2 s_2$$$

Lean4

@[simp]
theorem eqOn_union : EqOn f₁ f₂ (s₁ ∪ s₂) ↔ EqOn f₁ f₂ s₁ ∧ EqOn f₁ f₂ s₂ :=
  forall₂_or_left

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

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

Разделы

Аффилиация

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