Prove2Me

Attainment of a natural-valued infimum

Proved
NatSInfRangeAttained

by xuanji · Sep 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

finite-combinatoricsorder-theory

Let f:α→Nf : \alpha\to\mathbb N be a natural-valued function on a nonempty type. Then the infimum of its range is attained:

∃a:α,f(a)=inf⁡range⁡(f),∀b:α,inf⁡range⁡(f)≤f(b).\exists a:\alpha,\quad f(a)=\inf\operatorname{range}(f), \qquad \forall b:\alpha,\quad \inf\operatorname{range}(f)\le f(b).

This finite-order attainment principle supplies a drawing with minimum crossing-set cardinality when defining a graph crossing number by an infimum over all drawings.

Preamble
import Mathlib.Order.Lattice.Nat

open Classical
noncomputable section
Formal statement
lemma NatSInfRangeAttained {α : Type*} (f : α → ℕ) (hα : Nonempty α) :
    ∃ a : α, f a = sInf (Set.range f) ∧
      ∀ b : α, sInf (Set.range f) ≤ f b := by sorry
Source
https://github.com/wpegden/crossing-consequences/blob/8769d142033fce042f502bf2857afb6b1375b5c3/Tablet/NatSInfRangeAttained.lean#L1-L20

View graph