zpow_eq_empty — Mathlib

English

The z-power of a Finset is empty exactly when the Finset is empty and the exponent is nonzero.

Русский

z-степень Finset пустая тогда и только тогда, когда само Finset пусто и показатель n не равен нулю.

LaTeX

$$s^n = ∅ ⇔ s = ∅ ∧ n ≠ 0$$

Lean4

@[to_additive (attr := simp)]
theorem zpow_eq_empty : s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0 := by
  constructor
  · contrapose!
    rintro (hs | rfl)
    · exact nonempty_iff_ne_empty.1 (nonempty_iff_ne_empty.2 hs).zpow
    · rw [← nonempty_iff_ne_empty]
      simp
  · rintro ⟨rfl, hn⟩
    exact empty_zpow hn

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