English
For Finset s and natural n, s^n = ∅ if and only if s = ∅ and n ≠ 0.
Русский
Для множества Finset s и натурального n выполняется s^n = ∅ тогда и только тогда, когда s = ∅ и n ≠ 0.
LaTeX
$$$s^n = \\emptyset \\iff (s = \\emptyset \\land n \\neq 0)$$$
Lean4
@[to_additive (attr := simp)]
theorem pow_eq_empty : s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0 := by
constructor
· contrapose!
rintro
(hs | rfl)
-- TODO: The `nonempty_iff_ne_empty` would be unnecessary if `push_neg` knew how to simplify
-- `s ≠ ∅` to `s.Nonempty` when `s : Finset α`.
-- See https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/push_neg.20extensibility
· exact nonempty_iff_ne_empty.1 (nonempty_iff_ne_empty.2 hs).pow
· rw [← nonempty_iff_ne_empty]
simp
· rintro ⟨rfl, hn⟩
exact empty_pow hn
