biUnion_subset_biUnion_of_subset_left

Mathlib.Data.Finset.Union

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

English

If s1 ⊆ s2, then s1.biUnion t ⊆ s2.biUnion t for any t.

Русский

Если s1 ⊆ s2, то s1.biUnion t ⊆ s2.biUnion t для любого t.

LaTeX

$$$s_1 \\subseteq s_2 \\Rightarrow s_1.biUnion t \\subseteq s_2.biUnion t$$$

Lean4

theorem biUnion_subset_biUnion_of_subset_left (t : α → Finset β) (h : s₁ ⊆ s₂) : s₁.biUnion t ⊆ s₂.biUnion t := by grind

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

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

Разделы

Аффилиация

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