Cardinality of n, relating leq and le

Stream: Is there code for X?

[Michael Rothgang]

Informally: a cardinal number is at least n+1 iff it is greater than n.
Lean MWE:

import Mathlib
-- most general version
lemma leq_iff_le_succ {n : ℕ} {c : Cardinal} : n < c  ↔ n + 1 ≤ c := sorry

-- sufficient for my application
lemma Cardinal.leq_two_iff_le_one {c : Cardinal} : 2 ≤ c ↔ 1 < c := sorry

-- I can prove; that doesn't suffice for me as I need a cardinal `c` and not `mk α`
lemma foo {α : Type} : 2 ≤ Cardinal.mk α ↔ 1 < Cardinal.mk α := by
  rw [Cardinal.one_lt_iff_nontrivial, nontrivial_iff, Cardinal.two_le_iff]

To un-#xy, I'd like to translate between two statements about the rank of modules.

(If these lemmas should be named differently, I don't mind feedback about this either.)

[Kevin Buzzard]

import Mathlib

-- I can prove; that doesn't suffice for me as I need a cardinal `c` and not `mk α`
lemma foo {α : Type*} : 2 ≤ Cardinal.mk α ↔ 1 < Cardinal.mk α := by
  rw [Cardinal.one_lt_iff_nontrivial, nontrivial_iff, Cardinal.two_le_iff]

-- but every cardinal is of the form `mk α`
lemma Cardinal.leq_two_iff_le_one {c : Cardinal} : 2 ≤ c ↔ 1 < c := by
  refine Quotient.inductionOn c (fun α ↦ ?_)
  apply foo

[Kevin Buzzard]

for naming feedback, Cardinal.two_le_iff_one_lt is perhaps the name for it, and two_le_mk_iff_one_lt for foo.

[Ruben Van de Velde]

import Mathlib
-- most general version
lemma leq_iff_le_succ {n : ℕ} {c : Cardinal} : n < c  ↔ n + 1 ≤ c := by
  rw [← Nat.cast_one, ← Nat.cast_add]
  cases lt_or_le c Cardinal.aleph0 with
  | inl h =>
      obtain ⟨k, rfl⟩ := Cardinal.lt_aleph0.mp h
      rw [Nat.cast_le, Nat.cast_lt, Nat.succ_le]
  | inr h =>
      apply iff_of_true
      · exact lt_of_lt_of_le (Cardinal.nat_lt_aleph0 n) h
      · exact le_trans (Cardinal.nat_lt_aleph0 (n + 1)).le h

[Michael Rothgang]

Thank you, @Kevin Buzzard and @Ruben Van de Velde.
I'll need this for #11337, and have PRed these lemmas separately as #11544.

[Floris van Doorn]

We almost have this:

import Mathlib.SetTheory.Cardinal.Basic

lemma Cardinal.succ_natCast (n : ℕ) : Order.succ (n : Cardinal) = n + 1 := by
  rw [← Cardinal.nat_succ]
  norm_cast

lemma leq_iff_le_succ {n : ℕ} {c : Cardinal} : n < c ↔ n + 1 ≤ c := by
  rw [← Order.succ_le_iff, Cardinal.succ_natCast]

[Yaël Dillies]

Yes, this is the purpose of docs#SuccOrder

[Floris van Doorn]

I think both these lemmas are valuable to add. For leq_iff_le_succ I would reverse the iff and rename to Cardinal.natCast_add_one_le_iff.

[Yaël Dillies]

In fact, I had originally designed SuccOrder with succ n hardcoded as n + 1. I still think it's worth having as it will give more rewrite-friendly lemmas

[Yaël Dillies]

Certainly, it shouldn't be restricted to Cardinal

[Floris van Doorn]

Yaël Dillies said:

In fact, I had originally designed SuccOrder with succ n hardcoded as n + 1. I still think it's worth having as it will give more rewrite-friendly lemmas

For Cardinal that doesn't work. From the docstring:

Note that the successor of `c` is not the same as `c + 1` except in the case of finite `c`.

[Floris van Doorn]

Yaël Dillies said:

Certainly, it shouldn't be restricted to Cardinal

You are thinking of a generalization that I'm not thinking of? The only generalization I can think of is to introduce an AddOneClass or something, which I'm not sure is worth it.

[Yaël Dillies]

Ah right, it works for ordinals but not for cardinals :sad:

[Yaël Dillies]

Floris van Doorn said:

The only generalization I can think of is to introduce an AddOneClass or something

What I'm thinking of is something like

class AddSuccOrder (α : Type*) [PartialOrder α] [AddMonoidWithOne α] extends SuccOrder α where
  succ a := a + 1
  succ_eq_add_one a : succ a = a + 1 := by rfl

[Floris van Doorn]

Sure, that is a possible class to add, and maybe worth it

[Yaël Dillies]

This would apply to Int, Nat, Fin (n + 1), ZMod n, Ordinal

[Floris van Doorn]

Does it apply to Fin and ZMod (w.r.t. the largest element)?

[Yaël Dillies]

Yes, because the way docs#SuccOrder is set up means that succ a needs to be the successor element only if a is not maximal

[Floris van Doorn]

yes, but I thought for maximal elts succ a = a, and in at least one of Fin and ZMod, a+1=0 for the maximal elt a.

[Yaël Dillies]

Ah, I see what you mean. Make it succ_eq_add_one (a) (ha : ¬ IsMax a) : succ a = a + 1 := by rfl

[Floris van Doorn]

Floris van Doorn said:

in at least one of Fin and ZMod, a+1=0 for the maximal elt a.

This holds for both of them, right?

[Yaël Dillies]

(I am still in favor of equipping Fin n with saturating addition, btw...)

[Floris van Doorn]

Yes, I can see that, I'm not sure.

[Floris van Doorn]

Yaël Dillies said:

Ah, I see what you mean. Make it succ_eq_add_one (a) (ha : ¬ IsMax a) : succ a = a + 1 := by rfl

That by rfl will certainly not work when ha is needed to prove it :big_smile: But yeah, that could work. The lemma n < c ↔ n + 1 ≤ c still wouldn't hold unconditionally in Fin and ZMod.

[Floris van Doorn]

and for Nat/Int/Ordinal you would want an unconditional lemma (which I guess you get when assuming NoMaxOrder).

[Floris van Doorn]

It's a minor duplication that could be removed. I would approve it if someone does it, but I don't think it's very high priority. SuccOrder itself is very nice though.

[Yaël Dillies]

I abandoned the idea of AddSuccOrder back in 2021 not because it was bad but because I was bad (at Lean) and struggled with more basic things. I think it's worth doing (maybe you can do it as an order theory exercise, @Michael Rothgang?)

[Michael Rothgang]

Yaël Dillies said:

I abandoned the idea of AddSuccOrder back in 2021 not because it was bad but because I was bad (at Lean) and struggled with more basic things. I think it's worth doing (maybe you can do it as an order theory exercise, Michael Rothgang?)

Sure, but not soon :-) I'm on the final stretches of my thesis; that's too large a task for me right now. I'll put that on my list for later; feel free to remind me in June!