union_congr_left

Mathlib.Data.Finset.Lattice.Basic

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

English

If t ⊆ s ∪ u and u ⊆ s ∪ t, then s ∪ t = s ∪ u.

Русский

Если t ⊆ s ∪ u и u ⊆ s ∪ t, то s ∪ t = s ∪ u.

LaTeX

$$$(t \\subseteq s \\cup u) \\land (u \\subseteq s \\cup t) \\Rightarrow s \\cup t = s \\cup u$$$

Lean4

theorem union_congr_left (ht : t ⊆ s ∪ u) (hu : u ⊆ s ∪ t) : s ∪ t = s ∪ u :=
  sup_congr_left ht hu

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

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

Разделы

Аффилиация

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