commProb_pos — Mathlib

English

For a finite type M with a nonempty underlying set, the commuting probability is positive: 0 < commProb(M).

Русский

Для конечного типа M с непустым множеством элементов вероятность коммутирования положительна: 0 < commProb(M).

LaTeX

$$[Finite M, Nonempty M] ⇒ 0 < commProb(M)$$

Lean4

theorem commProb_pos [h : Nonempty M] : 0 < commProb M :=
  h.elim fun x ↦
    div_pos (Nat.cast_pos.mpr (Finite.card_pos_iff.mpr ⟨⟨(x, x), rfl⟩⟩)) (pow_pos (Nat.cast_pos.mpr Finite.card_pos) 2)

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