Well-founded Set

Stream: new members

[Karthik 🦋]

Hello! I need to prove that the { m : ℤ | f m ≥ n } is well-founded. The function f is strictly increasing, so the set is bounded below. Is there a lemma which lets me prove this by using the fact that natural numbers are well-founded? Or is there an easier way?

[Karthik 🦋]

To be more direct, I need the minimum of this set.

[Yaël Dillies]

I have #18604 open, but it doesn't seem to directly help here. Thinking...

[Ruben Van de Velde]

I managed it with @Yaël Dillies's lemma from #18604 after proving

lemma min_aux (n : ℤ) (f : ℤ → ℤ) (h : strict_mono f) :
  ∃ x, n < f x := sorry
lemma min_aux2 (n : ℤ) (f : ℤ → ℤ) (h : strict_mono f) :
  ∃ x, f x < n := sorry

Full proof (unpolished)

import group_theory.free_product
import group_theory.index
import order.locally_finite
import data.int.interval

section

variables {α : Type*} {s : set α} [preorder α] [locally_finite_order α]

open set

lemma bdd_below.well_founded_on_lt : bdd_below s → s.well_founded_on (<) := sorry

end

variables (n : ℤ) (f : ℤ → ℤ) (h : strict_mono f)
include n f h

lemma min_aux : ∃ x, n < f x :=
begin
  cases lt_or_le n (f 0) with h' h',
  { exact ⟨_, h'⟩ },
  revert n,
  apply int.le_induction,
  { use 1,
    apply h,
    norm_num },
  rintros n hn ⟨N, hN⟩,
  use (N + 1),
  calc n + 1 ≤ f N : hN
  ... < f (N + 1) : h (by norm_num),
end

lemma min_aux2 : ∃ x, f x < n :=
begin
  cases lt_or_le (f 0) n with h' h',
  { exact ⟨_, h'⟩ },
  revert n,
  apply int.le_induction_down,
  { use -1,
    apply h,
    norm_num },
  rintros n hn ⟨N, hN⟩,
  use (N - 1),
  calc n - 1 ≥ f N : by simp [int.le_sub_one_iff, hN]
  ... > f (N - 1) : h (by norm_num),
end


noncomputable def min' : ℤ :=
@set.is_wf.min _ _ { m : ℤ | f m ≥ n }
begin
  rw [set.is_wf],
  apply bdd_below.well_founded_on_lt,
  obtain ⟨N, nH⟩ := min_aux2 n f h,
  rw [bdd_below_def],
  simp,
  use N,
  intro y,
  refine not_imp_not.mp _,
  push_neg,
  intro hy,
  apply lt_trans _ nH,
  apply h hy,
end
begin
  rw [set.nonempty],
  apply Exists.imp _ (min_aux n f h),
  intros a ha,
  simp [ha.le],
end

lemma min'_le : ∀ m ∈ { m : ℤ | f m ≥ n }, min' n f h ≤ m :=
begin
  intros m hm,
  rw [min'],
  apply set.is_wf.min_le _ _ hm,
end

[Karthik 🦋]

Thank you!
I will try using this.

[Yaël Dillies]

I think I have a better proof, but I am still not finding the right generality for the argument.

[Violeta Hernández]

"a lower bounded set of integers is well-founded" isn't that the correct generality?

[Violeta Hernández]

The argument uses that you can put such a set in correspondence with a set of naturals

[Violeta Hernández]

I can't think of any more general procedure that would create an analog of integers for other well-founded orders

[Eric Wieser]

Is it true for any locally finite linear order?

[Raghuram Sundararajan]

Violeta Hernández said:

"a lower bounded set of integers is well-founded" isn't that the correct generality?

A big mess and specific to Int, but here's the proof (in Lean 4):

import Mathlib.Order.WellFoundedSet

lemma int_wf_of_lower_bound (s : Set ℤ) (a : ℤ) (h : a ∈ lowerBounds s)
    : s.IsWf :=
  -- Anything works in place of `.natAbs` as long as it sends non-negative
  -- integers to the corresponding natural numbers and we can easily
  -- prove that it does so.
  have : ∀ x : s, (x - a).natAbs = ↑x - a := fun ⟨_, h_x⟩ =>
    Eq.symm <| Int.eq_natAbs_of_zero_le <| Int.sub_nonneg_of_le (h h_x)
  have : (fun x y : s => (x:ℤ) < y) = Measure (fun x : s => x - a |>.natAbs) := by
    ext x y
    unfold Measure InvImage; dsimp; rewrite [←Int.ofNat_lt, this, this]
    show (x:ℤ) < y ↔ x - a < y - a  -- can't find a lemma for this, so proving it
    apply Iff.intro
    · apply Int.sub_lt_sub_right (c := a)
    · conv => rhs; rewrite [←Int.sub_add_cancel x a,
                            ←Int.sub_add_cancel y a]
      apply Int.add_lt_add_right (c := a)
  by unfold Set.IsWf Set.WellFoundedOn; rewrite [this]; apply IsWellFounded.wf

This uses the function Measure := fun (f : A -> Nat) => fun a1 a2 => f a1 < f a2, since mathlib knows Measure f is always well-founded.

[Raghuram Sundararajan]

Eric Wieser said:

Is it true for any locally finite linear order?

The pull request #18604 mentioned above seems to prove precisely this.

Also, the below (again Lean 4) shows that a lower-bounded set in a locally finite linear order is well-ordered in the sense of all non-empty subsets having a minimum. (It has one sorry.)

variable {α} [LinearOrder α] [LocallyFiniteOrder α]

example {s : Set α} {a : α} (h : a ∈ lowerBounds s)
        {s'} (h_sub : s' ⊆ s) (h' : s'.Nonempty)
    : ∃ c, IsLeast s' c :=
  have h : a ∈ lowerBounds s' := lowerBounds_mono_set h_sub h

  let b := Classical.choose h'
  have h_b : b ∈ s' := Classical.choose_spec h'

  let finiteSet := s' ∩ Set.Icc a b
  have h_b_f : b ∈ finiteSet :=
    Set.mem_inter h_b (Set.right_mem_Icc.mpr (h h_b))
  have : finiteSet.Finite :=
    /- it is a subset of Set.Icc a b, which is finite -/
    have : ∀ {s t : Set α}, t.Finite → (s ∩ t).Finite :=
      sorry
    this (Set.finite_Icc a b)

  let ⟨min, h_min_mem, h_min_le⟩ :=
    finiteSet.exists_min_image id this (Set.nonempty_of_mem h_b_f)
  have h_min_mem : min ∈ s' := Set.inter_subset_left _ _ h_min_mem
  have h_min_le : min ∈ lowerBounds s' := fun c h_c =>
    match le_total b c with
    | .inl h' => calc min ≤ b := h_min_le b h_b_f
                        _ ≤ c := h'
    | .inr h' =>
      h_min_le c <| show c ∈ finiteSet from
                    Set.mem_inter h_c ⟨h h_c, h'⟩

  ⟨min, h_min_mem, h_min_le⟩

[Ruben Van de Velde]

One which looks like docs4#Set.Finite.inter_of_right

[Raghuram Sundararajan]

Not sure how I missed that :sweat_smile: