English
For a fixed n, an m is in s.sym n iff every element of m lies in s.
Русский
Для фиксированного n элемент m принадлежит s.sym n тогда и только тогда, когда каждый элемент m принадлежит s.
LaTeX
$$m ∈ s^{(n)} \iff \forall a \in m, a \in s$$
Lean4
@[simp]
theorem mem_sym_iff {m : Sym α n} : m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s :=
by
induction n with
| zero =>
refine mem_singleton.trans ⟨?_, fun _ ↦ Sym.eq_nil_of_card_zero _⟩
rintro rfl
exact fun a ha ↦ (Finset.notMem_empty _ ha).elim
| succ n ih => ?_
refine mem_sup.trans ⟨?_, fun h ↦ ?_⟩
· rintro ⟨a, ha, he⟩ b hb
rw [mem_image] at he
obtain ⟨m, he, rfl⟩ := he
rw [Sym.mem_cons] at hb
obtain rfl | hb := hb
· exact ha
· exact ih.1 he _ hb
· obtain ⟨a, m, rfl⟩ := m.exists_eq_cons_of_succ
exact
⟨a, h _ <| Sym.mem_cons_self _ _, mem_image_of_mem _ <| ih.2 fun b hb ↦ h _ <| Sym.mem_cons_of_mem hb⟩
-- @[simp] /- adaption note for https://github.com/leanprover/lean4/pull/8419: the simpNF complained -/
