union — Mathlib

English

Let f1, f2: α → β and s1, s2 ⊆ α. If f1 and f2 agree on s1 and also on s2, then they agree on s1 ∪ s2.

Русский

Пусть f1, f2: α → β и s1, s2 ⊆ α. Если f1 и f2 совпадают на s1 и также на s2, то они совпадают на объединении s1 ∪ s2.

LaTeX

$$$ \\forall f_1 f_2 : \\alpha \\to \\beta, \\ \\forall s_1 s_2 : Set \\alpha,\\ (EqOn\\ f_1\\ f_2\\ s_1) \\to (EqOn\\ f_1\\ f_2\\ s_2) \\to EqOn\\ f_1\\ f_2\\ (s_1 \\cup s_2) $$$

Lean4

theorem union (h₁ : EqOn f₁ f₂ s₁) (h₂ : EqOn f₁ f₂ s₂) : EqOn f₁ f₂ (s₁ ∪ s₂) :=
  eqOn_union.2 ⟨h₁, h₂⟩

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