sup_eq_union

Mathlib.Data.Finset.Lattice.Basic

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

English

For Finset α, the join operation s ⊔ t equals the union s ∪ t.

Русский

Для Finset α операция объединения двух множеств равна объединению их как множеств: s ⊔ t = s ∪ t.

LaTeX

$$$s \\sqcup t = s \\cup t$$$

Lean4

@[grind =]
theorem sup_eq_union {s t : Finset α} : s ⊔ t = s ∪ t :=
  rfl

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

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

Разделы

Аффилиация

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