Finite-set infimum comparison

Definition

KLSModular_BrownianMotion_Auxiliary_FiniteInf

by Lazyfill · Oct 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-contextvendored-brownianmotion

Vendored from RemyDegenne/brownian-motion at commit a7ad7af662044313bc80a7c0756360fb3745f931 under Apache-2.0. Set.Finite.lt_iInf_iff characterizes $a<\inf_{i∈s}f(i)$ for a nonempty finite set s in a complete linear order by the pointwise conditions $a<f(x)$ for every $x∈s$ .

Original module imports

public import Mathlib.Data.Finset.Max
public import Mathlib.Data.Set.Finite.Lattice
public import Mathlib.Order.CompletePartialOrder
public import Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
import Mathlib.Order.ConditionallyCompleteLattice.Finset

Original declaration excerpt

Shown in the original module context.

lemma Set.Finite.lt_iInf_iff {α ι : Type*} [CompleteLinearOrder α]
    {s : Set ι} {f : ι → α} (h : s.Nonempty) (hs : s.Finite) {a : α} :
    a < ⨅ i ∈ s, f i ↔ ∀ x ∈ s, a < f x := by
  rw [Set.Finite.lt_ciInf_iff hs]
  simpa

Module navigation

Project result: The KLS conjecture.

Original module · BrownianMotion.Auxiliary.FiniteInf · Frozen source 408915f.

Definition code

import Mathlib.Data.Finset.Max
import Mathlib.Data.Set.Finite.Lattice
import Mathlib.Order.CompletePartialOrder
import Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
import Mathlib.Order.ConditionallyCompleteLattice.Finset

-- Vendored from https://github.com/RemyDegenne/brownian-motion at commit a7ad7af662044313bc80a7c0756360fb3745f931 (upstream path BrownianMotion/Auxiliary/FiniteInf.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
section
variable {α ι : Type*} [CompleteLinearOrder α]
lemma Set.Finite.lt_iInf_iff {α ι : Type*} [CompleteLinearOrder α]
    {s : Set ι} {f : ι → α} (h : s.Nonempty) (hs : s.Finite) {a : α} :
    a < ⨅ i ∈ s, f i ↔ ∀ x ∈ s, a < f x := by
  rw [Set.Finite.lt_ciInf_iff hs]
  simpa

Source

Lean source: https://github.com/RemyDegenne/brownian-motion/blob/a7ad7af662044313bc80a7c0756360fb3745f931/BrownianMotion/Auxiliary/FiniteInf.lean#L57-L61 (repository human-ai-mathematics/kls-lean, commit 408915f, module `BrownianMotion.Auxiliary.FiniteInf`, definition bundle `KLSModular_BrownianMotion_Auxiliary_FiniteInf`; the repository is private at upload time). Vendored from https://github.com/RemyDegenne/brownian-motion at commit a7ad7af662044313bc80a7c0756360fb3745f931 (Apache-2.0; upstream copyright notice retained in the Lean text).

View graph