mem_sections — Mathlib

English

For any s ∈ Multiset (Multiset α) and any a, a is in Sections s if and only if s.Rel (λ s a, a ∈ s) a.

Русский

Для любого s ∈ Multiset(Multiset α) и любого a, a входит в Sections s тогда и только тогда, когда s Rel (λ s a, a ∈ s) a.

LaTeX

$$$$ a \\in \\operatorname{Sections}(s) \\iff s \\operatorname{Rel} (\\lambda s a. a \\in s) a. $$$$

Lean4

theorem mem_sections {s : Multiset (Multiset α)} : ∀ {a}, a ∈ Sections s ↔ s.Rel (fun s a => a ∈ s) a := by
  induction s using Multiset.induction_on with
  | empty => simp
  | cons _ _ ih => simp [ih, rel_cons_left, eq_comm]

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