instUnion — Mathlib

English

The union of Finset α is defined as the set of elements belonging to either operand; i.e., a ∈ s ∪ t iff a ∈ s or a ∈ t.

Русский

Объединение множества Finset α определяется как множество элементов, принадлежащих хотя бы одному из множителей; то есть a ∈ s ∪ t тогда и только тогда, когда a ∈ s или a ∈ t.

LaTeX

$$$\\forall s,t:\\, (a\\in s \\cup t) \\iff (a\\in s) \\lor (a\\in t)$$$

Lean4

/-- `s ∪ t` is the set such that `a ∈ s ∪ t` iff `a ∈ s` or `a ∈ t`. -/
instance : Union (Finset α) :=
  ⟨fun s t => ⟨_, t.2.ndunion s.1⟩⟩

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