union_eq_right

Mathlib.Data.Finset.Lattice.Basic

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

English

Equality S ∪ T = T holds iff S ⊆ T.

Русский

Равенство S ∪ T = T выполняется тогда и только тогда, когда S ⊆ T.

LaTeX

$$$s \\cup t = t \\iff s \\subseteq t$$$

Lean4

@[simp]
theorem union_eq_right : s ∪ t = t ↔ s ⊆ t :=
  sup_eq_right

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

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

Разделы

Аффилиация

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