pimage_congr

Mathlib.Data.Finset.PImage

URI: https://scilib.ai/kg/mathlib#Finset.pimage_congr

English

If s = t and f = g on t, then s.pimage f = t.pimage g.

Русский

Если s = t и для всех x в t имеет место f x = g x, то s.pimage f = t.pimage g.

LaTeX

$$$s = t \Rightarrow (\forall x\in t, f x = g x) \Rightarrow s.pimage f = t.pimage g$.$$

Lean4

theorem pimage_congr (h₁ : s = t) (h₂ : ∀ x ∈ t, f x = g x) : s.pimage f = t.pimage g := by aesop

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

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

Разделы

Аффилиация

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