English
The disjUnion s t h is the finite set consisting of elements of s or t (no duplication since s and t are disjoint).
Русский
Объединение disjUnion s t h есть множество, содержащее элементы из s или из t без повторений, так как s и t непересекаются.
LaTeX
$$$a \\in \\operatorname{disjUnion}(s,t,h) \\iff a \\in s \\lor a \\in t$$$
Lean4
/-- `disjUnion s t h` is the set such that `a ∈ disjUnion s t h` iff `a ∈ s` or `a ∈ t`.
It is the same as `s ∪ t`, but it does not require decidable equality on the type. The hypothesis
ensures that the sets are disjoint. -/
@[simps]
def disjUnion (s t : Finset α) (h : Disjoint s t) : Finset α :=
⟨s.1 + t.1, Multiset.nodup_add.2 ⟨s.2, t.2, disjoint_val.2 h⟩⟩
