inter_preimage_eq

Mathlib.Data.Set.Function

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

English

If EqOn f1 f2 on s, then s ∩ f1⁻¹'(t) = s ∩ f2⁻¹'(t) for any t.

Русский

Если EqOn f1 f2 на s, то для любого t выполняется s ∩ f1⁻¹'(t) = s ∩ f2⁻¹'(t).

LaTeX

$$$ \mathrm{EqOn}\, f_1 f_2 s \rightarrow \forall t, \; s \cap f_1^{-1}(t) = s \cap f_2^{-1}(t)$$$

Lean4

theorem inter_preimage_eq (heq : EqOn f₁ f₂ s) (t : Set β) : s ∩ f₁ ⁻¹' t = s ∩ f₂ ⁻¹' t := by grind

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

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

Разделы

Аффилиация

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