image_eq

Mathlib.Data.Set.Function

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

English

If EqOn f1 f2 on s, then images of s under f1 and f2 are equal sets.

Русский

Если EqOn f1 f2 на s, то образы s под f1 и f2 совпадают.

LaTeX

$$$ \mathrm{EqOn}\, f_1 f_2 s \rightarrow f_1 '' s = f_2 '' s$$$

Lean4

theorem image_eq (heq : EqOn f₁ f₂ s) : f₁ '' s = f₂ '' s := by grind

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

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

Разделы

Аффилиация

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