EqOn

Mathlib.Data.Set.Operations

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

← MathLib Explorer

English

EqOn(f1,f2,s) holds iff f1 x = f2 x for all x ∈ s.

Русский

EqOn(f1,f2,s) эквивалентно f1(x) = f2(x) для всех x ∈ s.

LaTeX

$$$$\\mathrm{EqOn}(f_1,f_2,s) \\;=\\; \\forall x \\in s,\\; f_1(x)=f_2(x).$$$$

Lean4

/-- Two functions `f₁ f₂ : α → β` are equal on `s` if `f₁ x = f₂ x` for all `x ∈ s`. -/
def EqOn (f₁ f₂ : α → β) (s : Set α) : Prop :=
  ∀ ⦃x⦄, x ∈ s → f₁ x = f₂ x

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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