ndunion_le — Mathlib

English

For all s,t,u, ndunion s t ≤ u iff s ⊆ u and t ≤ u.

Русский

Для всех s,t,u: ndunion s t ≤ u эквивалентно s ⊆ u и t ≤ u.

LaTeX

$$$\\mathrm{ndunion}(s,t) \\le u \\iff s \\subseteq u \\land t \\le u$$$

Lean4

theorem ndunion_le {s t u : Multiset α} : ndunion s t ≤ u ↔ s ⊆ u ∧ t ≤ u :=
  Multiset.induction_on s (by simp [zero_ndunion])
    (fun _ _ h => by simp only [cons_ndunion, ndinsert_le, and_comm, cons_subset, and_left_comm, h, and_assoc])

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