ENat.iSup_eq_coe_iff

Stream: Is there code for X?

[Joachim Breitner]

I feel like this lemma should be more straight forward than any of my partial attempts would lead to, so maybe someone here can help me out? (If the non-empty Sup of a ENat is a Nat, then it’s actually a maximum)

import Mathlib.Data.ENat.Lattice
lemma ENat.iSup_eq_coe_iff' {α : Type*} [Nonempty α] (f : α → ℕ∞) (n : ℕ) :
    (⨆ x, f x = n) ↔ (∃ x, f x = n) ∧ (∀ y, f y ≤ n) := by
  sorry

[Gareth Ma]

Surely it's false if $\alpha$ is not finite? $f(n) = 1 - \frac{1}{n}$

[Yaël Dillies]

Look at the codomain of f :wink:

[Gareth Ma]

Ah oops llol

[Gareth Ma]

Okay I tried for a bit and failed miserably, but I think an approach that’s fun and good for Mathlib would be to prove ENat is compact. I think you can prove this by constructing a homeomorphism between ENat and Nat (reminds me of Hilbert’s infinite hotel thing). We don’t even know that ENat is discrete right now lol

[Joachim Breitner]

At least good to know that it isn't embarrassing trivial :-)

[Yaël Dillies]

I definitely have proved this before. Let me switch on my brain

[Gareth Ma]

I think this can be generalised by replacing Nat and ENat by types A and B with an order-preserving embedding (injective) A -> B, in place of Nat.cast.

example {s : Set ℕ∞} (hs : Nonempty s) (hs' : sSup s < ⊤) : sSup s ∈ s := by
  -- Since sSup < ⊤, sSup = ↑k
  obtain ⟨k, hk⟩ : ∃ k : ℕ, sSup s = k := Option.ne_none_iff_exists'.mp hs'.ne
  -- Now we look at Nat.cast ⁻¹' s, i.e. forcing s "down" to Set ℕ
  have h_bdd : BddAbove (Nat.cast ⁻¹' s) := by
    use k
    simp [mem_upperBounds]
    intro x h
    have : (x : ℕ∞) ≤ k := by
      simp_rw [← hk]
      exact CompleteLattice.le_sSup s (↑x) h
    exact_mod_cast this
  have h_lt_top {a : ℕ∞} (ha : a ∈ s) : a < ⊤ :=
    lt_of_le_of_lt (hk ▸ CompleteLattice.le_sSup s a ha) (lt_of_eq_of_lt hk.symm hs')
  have h_top : ⊤ ∉ s := by
    by_contra! h
    exact (lt_self_iff_false ⊤).mp (h_lt_top h)
  have h_sSup_eq_some := WithTop.sSup_eq (s := s) h_top (by simpa using h_bdd)
  rw [hk, ENat.some_eq_coe, Nat.cast_inj] at h_sSup_eq_some
  -- Here we transfer the problem to Set ℕ, for which sSup s ∈ s
  have h_nonempty : (Nat.cast ⁻¹' s).Nonempty := by
    obtain ⟨a, ha⟩ := Classical.choice hs
    obtain ⟨k, hk⟩ : ∃ k : ℕ, a = k := Option.ne_none_iff_exists'.mp (h_lt_top ha).ne
    use k, by simp [← hk, ha]
  have h_mem := Nat.sSup_mem (s := Nat.cast ⁻¹' s) h_nonempty h_bdd
  rwa [Set.mem_preimage, ← h_sSup_eq_some, ← hk] at h_mem

[Gareth Ma]

But yeah as I said probably proving results about WithTop (X : some topological space), e.g. that it's compact when X is WithBot + some strong linear ordering (somewhere under CompleteLattice), will be good.

[Gareth Ma]

More Mathlib-y

[Rida Hamadani]

Do we have anything in mathlib related to Alexandroff extensions? I think that would be the nicest way to formalize this.

[Gareth Ma]

I updated the proof above, now it's at least decent quality, and also rephrased the original question. But I still think it's not the best approach for Mathlib, for which I will leave for experts ^

[Ruben Van de Velde]

"Alexandrov" has several hits, but not sure if any of them are relevant

[Rida Hamadani]

I couldn't find anything relevant. I meant this. The "see also" section of this page includes a proof of compactness.

[Rida Hamadani]

We could use that to show that ENat is compact (since it is the Alexandroff extension of Nat).

[Gareth Ma]

Speaking of which, can someone prove that IsOpen (Set.Ici (n : ENat))? I cannot understand the second goal or the API around it at all.

example : IsOpen (Set.Ici (3 : ENat)) := by
  use ?_, ?_
  · intro x y h h'; simp_all; exact h'.trans h
  · sorry

[Etienne Marion]

Rida Hamadani said:

I couldn't find anything relevant. I meant this. The "see also" section of this page includes a proof of compactness.

This is docs#OnePoint.

[Rida Hamadani]

Thank you!

[Etienne Marion]

See also https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Topology.20of.20.60ENat.60 for a discussion about ENat topology. You can equip it with order topology, which automatically infers compactness.

[Joachim Breitner]

Here is a naive proof.

import Mathlib.Data.ENat.Lattice
import Mathlib.Tactic.NormNum.Core

theorem ENat.lt_add_one_iff (n m : ℕ∞) (hm : n ≠ ⊤) : m < n + 1 ↔ m ≤ n := by
  cases n <;> cases m <;> try contradiction
  · norm_num
  · norm_cast; omega


lemma ENat.iSup_eq_coe_iff' {α : Type*} [Nonempty α] (f : α → ℕ∞) (n : ℕ) :
    (⨆ x, f x = n) ↔ (∃ x, f x = n) ∧ (∀ y, f y ≤ n) := by
  constructor
  · intro h
    have hle : ∀ (y : α), f y ≤ ↑n := by
      replace h : ⨆ x, f x ≤ n := by simp [h]
      rw [iSup_le_iff] at h
      assumption
    simp only [hle, implies_true, and_true]
    by_contra! hnotn
    cases n with
    | zero =>
      specialize hle Classical.ofNonempty
      specialize hnotn Classical.ofNonempty
      simp_all
    | succ n =>
      suffices ⨆ x, f x < n+1 by simp_all
      rw [ENat.lt_add_one_iff _ _ (by simp)]
      rw [iSup_le_iff] at *
      intro i
      specialize hnotn i
      specialize hle i
      generalize f i = m at *
      cases m
      · simp_all
      · simp_all; norm_cast at *; omega
  · intro ⟨⟨x, hx⟩, h2⟩
    apply le_antisymm
    · rw [iSup_le_iff]
      intro i; exact h2 i
    ·apply le_iSup_of_le x (by simp [hx])

Is this worth mathlibbing, or is it too pedestrian / too ungeneralized?

[Gareth Ma]

I think the result should be stated as my second version, with sSup s \in s.

[Joachim Breitner]

Ok, I’ll see how well that works for my use cases

[Gareth Ma]

I think you can recover your statement form that directly. iSup f (indexed sup, the \Sup you wrote) is defined as sSup (Set.range f), so sSup (Set.range f) \in Set.range f means there exists x such that f x = iSup f = n, proving the first part. The second part (f y <= n) is trivial and true for any sup

[Johan Commelin]

ENat is infinite. So it cannot be compact and discrete at the same time. You can add a discrete point at infinity, and then you get a discrete space. Or you add a compactifying point at infinity, and then you get a compact space... But you can't do both at the same time.

[Joachim Breitner]

Gareth Ma said:

I think the result should be stated as my second version, with sSup s \in s.

Ok, gave it another shot. I found docs#Nonempty.csSup_mem to be a promising shortcut

lemma sSup_eq_top_of_infinite (h : s.Infinite) : sSup s = ⊤ := by
  apply (sSup_eq_top ..).mpr
  intro x hx
  cases x; simp at hx; next x =>
  contrapose! h
  simp only [not_infinite]
  apply Finite.subset <| Finite.Set.finite_image {n : ℕ | n ≤ x} (fun (n : ℕ) => (n : ℕ∞))
  intro y hy
  specialize h y hy
  have hxt : y < ⊤ := lt_of_le_of_lt h hx
  use y.toNat
  simp [toNat_le_of_le_coe h, LT.lt.ne_top hxt]

lemma finite_of_sSup_lt_top (h : sSup s < ⊤) : s.Finite := by
  contrapose! h
  simp only [top_le_iff]
  exact sSup_eq_top_of_infinite h

lemma sSup_mem_of_Nonempty_of_lt_top [Nonempty s] (hs' : sSup s < ⊤) : sSup s ∈ s :=
  Nonempty.csSup_mem nonempty_of_nonempty_subtype (finite_of_sSup_lt_top hs')

Put that up for review at https://github.com/leanprover-community/mathlib4/pull/15347