binEntropy_eq_zero — Mathlib

English

binEntropy(p) = 0 iff p ∈ {0,1}.

Русский

binEntropy(p) = 0 тогда и только тогда, когда p ∈ {0,1}.

LaTeX

$$$\mathrm{binEntropy}(p) = 0 \iff p = 0 \lor p = 1$$$

Lean4

theorem binEntropy_eq_zero : binEntropy p = 0 ↔ p = 0 ∨ p = 1 :=
  by
  refine ⟨fun h ↦ ?_, by rintro (rfl | rfl) <;> simp⟩
  contrapose! h
  obtain hp₀ | hp₀ := h.1.lt_or_gt
  · exact (binEntropy_neg_of_neg hp₀).ne
  obtain hp₁ | hp₁ := h.2.lt_or_gt.symm
  · exact (binEntropy_neg_of_one_lt hp₁).ne
  · exact (binEntropy_pos hp₀ hp₁).ne'

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