mapsTo_iff

Mathlib.Data.Set.Function

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

English

If f1 and f2 agree on s, then MapsTo f1 s t and MapsTo f2 s t are equivalent statements.

Русский

Если f1 и f2 согласны на s, то MapsTo f1 s t и MapsTo f2 s t эквивалентны.

LaTeX

$$$ EqOn\\ f_1\\ f_2\\ s \\to (MapsTo\\ f_1\\ s\\ t \\leftrightarrow MapsTo\\ f_2\\ s\\ t) $$$

Lean4

theorem mapsTo_iff (H : EqOn f₁ f₂ s) : MapsTo f₁ s t ↔ MapsTo f₂ s t :=
  ⟨fun h => h.congr H, fun h => h.congr H.symm⟩

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

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

Разделы

Аффилиация

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