restrict_eq_restrict_iff

Mathlib.Data.Set.Restrict

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

English

Equality of restrictions to s is equivalent to equality of the original functions on s.

Русский

Равенство ограничений до s эквивалентно равенству исходных функций на s.

LaTeX

$$$\\text{restrict }s\\ f_1 = \\text{restrict }s\\ f_2 \\;\\iff\\; EqOn\\ f_1 f_2 s$$

Lean4

@[simp]
theorem restrict_eq_restrict_iff : restrict s f₁ = restrict s f₂ ↔ EqOn f₁ f₂ s :=
  restrict_eq_iff

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

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

Разделы

Аффилиация

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