English
For any a, s, h, and b, b ∈ s.cons a h iff b = a or b ∈ s.
Русский
Для любых a, s, h и b верно: b ∈ s.cons a h эквивалентно b = a или b ∈ s.
LaTeX
$$$\forall \{a,b:\alpha\}, \forall s:\ Finset\alpha, \forall h:\ Not (b\in s),\ (b \in s.cons a h) \iff (b = a) \lor (b \in s)$$$
Lean4
/-- `cons a s h` is the set `{a} ∪ s` containing `a` and the elements of `s`. It is the same as
`insert a s` when it is defined, but unlike `insert a s` it does not require `DecidableEq α`,
and the union is guaranteed to be disjoint. -/
def cons (a : α) (s : Finset α) (h : a ∉ s) : Finset α :=
⟨a ::ₘ s.1, nodup_cons.2 ⟨h, s.2⟩⟩
