sym_nonempty — Mathlib

English

Let s be a finite set. The n-th symmetric power of s is nonempty precisely when n = 0 or s is nonempty.

Русский

Пусть s — конечное множество. Н-нная симметрическая мощность множества s существуют тогда и только тогда, когда n = 0 или s непусто.

LaTeX

$$$ (s^{(n)}) \\neq \\emptyset \\iff n = 0 \\lor s \\neq \\emptyset $$$

Lean4

@[simp]
theorem sym_nonempty : (s.sym n).Nonempty ↔ n = 0 ∨ s.Nonempty := by
  simp only [nonempty_iff_ne_empty, ne_eq, sym_eq_empty, not_and_or, not_ne_iff]

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