le_singleton — Mathlib

English

A multiset s is below the singleton {a} exactly when s is either empty or equal to {a}.

Русский

Мультимножество s лежит ниже {a} тогда и только тогда, когда s пусто или равно {a}.

LaTeX

$$s \le {a} \iff s = 0 \lor s = {a}$$

Lean4

@[simp]
theorem le_singleton : s ≤ { a } ↔ s = 0 ∨ s = { a } :=
  Quot.induction_on s fun l ↦ by
    simp only [← coe_singleton, quot_mk_to_coe'', coe_le, coe_eq_zero, coe_eq_coe, perm_singleton,
      subperm_singleton_iff]

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