biUnion_congr

Mathlib.Data.Finset.Union

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

English

If s1 = s2 and t1 a = t2 a for all a ∈ s1, then s1.biUnion t1 = s2.biUnion t2.

Русский

Если s1 = s2 и t1 a = t2 a для всех a ∈ s1, то s1.biUnion t1 = s2.biUnion t2.

LaTeX

$$$\\text{biUnion_congr} (hs : s_1 = s_2) (ht : \\forall a \\in s_1, t_1 a = t_2 a) : s_1.biUnion t_1 = s_2.biUnion t_2$$$

Lean4

theorem biUnion_congr (hs : s₁ = s₂) (ht : ∀ a ∈ s₁, t₁ a = t₂ a) : s₁.biUnion t₁ = s₂.biUnion t₂ := by aesop

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

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

Разделы

Аффилиация

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