coe_infsep_of_offDiag_empty — Mathlib

English

If s.offDiag = ∅, then s.infsep = 0.

Русский

Если s.offDiag равно пустому множеству, то s.infsep равно 0.

LaTeX

$$$\displaystyle (s:\mathrm{Set}\alpha).infsep = 0 \quad\text{если } s.offDiag = \varnothing$$$

Lean4

theorem _root_.Finset.coe_infsep_of_offDiag_empty [DecidableEq α] {s : Finset α} (hs : s.offDiag = ∅) :
    (s : Set α).infsep = 0 := by
  rw [← Finset.not_nonempty_iff_eq_empty] at hs
  rw [Finset.coe_infsep, dif_neg hs]

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