disjSum — Mathlib

English

Disjoint sum of finsets s and t is the finset of pairs formed from s and t, living in the sum type α ⊕ β.

Русский

Дисъюнктное сумма двух Finset s и t равна Finset (α ⊕ β) получаемая из элементов s и t в декартовом произведении суммы типов.

LaTeX

$$disjSum : Finset (α ⊕ β) = ⟨s.1.disjSum t.1, s.2.disjSum t.2⟩$$

Lean4

/-- Disjoint sum of finsets. -/
def disjSum : Finset (α ⊕ β) :=
  ⟨s.1.disjSum t.1, s.2.disjSum t.2⟩

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