einfsep_eq_iInf — Mathlib

English

The Einfsep of a set equals the infimum over all ordered pairs from the set (excluding equal coordinates): einfsep(s) = inf_{(x,y) ∈ s×s, x ≠ y} edist(x,y).

Русский

Einfsep множества равен инфимума по всем упорядоченным парам из множества (с условием x ≠ y): einfsep(s) = inf_{(x,y)∈s×s, x≠y} edist(x,y).

LaTeX

$$$ \operatorname{einfsep}(s) = \inf_{(x,y) \in s\times s,\; x \neq y} \operatorname{edist}(x,y) $$$

Lean4

theorem einfsep_eq_iInf : s.einfsep = ⨅ d : s.offDiag, (uncurry edist) (d : α × α) :=
  by
  refine eq_of_forall_le_iff fun _ => ?_
  simp_rw [le_einfsep_iff, le_iInf_iff, imp_forall_iff, SetCoe.forall, mem_offDiag, Prod.forall, uncurry_apply_pair,
    and_imp]

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