mono

Mathlib.Data.Set.Function

URI: https://scilib.ai/kg/mathlib#Set.EqOn.mono

English

If s1 ⊆ s2 and f1 ≡ f2 on s2, then they are equal on s1.

Русский

Если s1 ⊆ s2 и f1 = f2 на s2, то на s1 они равны.

LaTeX

$$$ \text{Subset}(s_1,s_2) \rightarrow \mathrm{EqOn}\, f_1 f_2 s_2 \rightarrow \mathrm{EqOn}\, f_1 f_2 s_1$$$

Lean4

theorem mono (hs : s₁ ⊆ s₂) (hf : EqOn f₁ f₂ s₂) : EqOn f₁ f₂ s₁ := fun _ hx => hf (hs hx)

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

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

Разделы

Аффилиация

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