sym_eq_empty — Mathlib

English

The sym2 equals empty if and only if n is nonzero and the set is empty.

Русский

Sym2 равен пустоте тогда и только если n ≠ 0 и множество пусто.

LaTeX

$$s.sym n = ∅ \iff n \neq 0 \land s = ∅$$

Lean4

@[simp]
theorem sym_eq_empty : s.sym n = ∅ ↔ n ≠ 0 ∧ s = ∅ := by
  cases n
  · exact iff_of_false (singleton_ne_empty _) fun h ↦ (h.1 rfl).elim
  · refine ⟨fun h ↦ ⟨Nat.succ_ne_zero _, eq_empty_of_sym_eq_empty h⟩, ?_⟩
    rintro ⟨_, rfl⟩
    exact sym_empty _

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