infsep_of_fintype — Mathlib

English

If α is a type with decidable equality and s is finite and nontrivial, infsep equals the corresponding finite inf' over offDiag.

Русский

Если α имеет разрешимое равенство и s конечен и не тривиален, infsep равен соответствующему конечному inf' по offDiag.

LaTeX

$$$ [DecidableEq \alpha] [Fintype s] (hs : s.Nontrivial) : s.infsep = s.offDiag.toFinset.inf' (by simpa) (uncurry dist) $$$

Lean4

theorem infsep_of_fintype [DecidableEq α] [Fintype s] (hs : s.Nontrivial) :
    s.infsep = s.offDiag.toFinset.inf' (by simpa) (uncurry dist) := by classical rw [Set.infsep_of_fintype, dif_pos hs]

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