Weakening assumption of regular cardinal

Stream: maths

[Josha Dekker]

Hi, I was wondering if it is possible to weaken the assumption hc in `card_iUnion_lt_iff_forall_of_isRegular in docs#Cofinality, to something like (hc : ℵ₀ ≤ c)

Phrased in terms of a MWE, I wish to replace (hc : c.IsRegular) in card_iUnion_lt_iff_forall_of_isRegular by a strictly weaker assumption (as weak as possible) in card_iUnion_lt_iff_forall_of_isRegular2. I'm certainly willing to assume (hc : ℵ₀ ≤ c)

This is the crucial element because of which I needed Cardinal.IsRegular in multiple occasions in CardinalInterFilter and I'm running into the same issue for κ-Lindelöf spaces, so I wanted to ensure that this assumption is in fact minimal.

import Mathlib.SetTheory.Cardinal.Cofinality

universe u

open Cardinal

variable {ι : Type}

@[simp]
theorem card_iUnion_lt_iff_forall_of_isRegular {ι : Type u} {α : Type u} {t : ι → Set α}
    {c : Cardinal} (hc : c.IsRegular) (hι : #ι < c) : #(⋃ i, t i) < c ↔ ∀ i, #(t i) < c := by
  refine ⟨card_lt_of_card_iUnion_lt, fun h ↦ ?_⟩
  apply lt_of_le_of_lt (Cardinal.mk_sUnion_le _)
  apply Cardinal.mul_lt_of_lt hc.aleph0_le
    (lt_of_le_of_lt Cardinal.mk_range_le hι)
  apply Cardinal.iSup_lt_of_isRegular hc (lt_of_le_of_lt Cardinal.mk_range_le hι)
  simpa

@[simp]
theorem card_iUnion_lt_iff_forall_of_isRegular2 {ι : Type u} {α : Type u} {t : ι → Set α}
    {c : Cardinal} (hc : ℵ₀ ≤ c) (hι : #ι < c) : #(⋃ i, t i) < c ↔ ∀ i, #(t i) < c := by
  refine ⟨card_lt_of_card_iUnion_lt, fun h ↦ ?_⟩
  apply sorry

[Antoine Chambert-Loir]

I'd just try to prove the statement from basic properties on cardinals : the cardinal of a union of ≤ c many sets of cardinalities ≤ c' is ≤ c * c'.

[Josha Dekker]

Antoine Chambert-Loir said:

I'd just try to prove the statement from basic properties on cardinals : the cardinal of a union of ≤ c many sets of cardinalities ≤ c' is ≤ c * c'.

Yes, but how do I do pass from strict inequality to weak inequalities? That’d require finding some largest cardinal smaller than k. Is that possible/do we have this?

[Anatole Dedecker]

Yes the point is that we want a strict inequality

[Josha Dekker]

The following works to go down to a lower cardinality, let me check if I can simplify the proof!

theorem small_card (c : Cardinal) (S : Set α) (hS : #S < c) : ∃ k, #S ≤ k ∧ k < c := by
  apply Exists.intro
  apply And.intro
  · exact partialOrder.proof_1 #↑S
  · exact hS

[Anatole Dedecker]

This lemma doesn’t help much since you could always take k to be the cardinal of S, right ?

[Josha Dekker]

Anatole Dedecker said:

This lemma doesn’t help much since you could always take k to be the cardinal of S, right ?

Yes, that’s true, and I guess taking a supremum might be problematic…

[Anatole Dedecker]

I’m not super fluent with cardinal arithmetics, but thinking a bit about it, I think your original statement is equivalent to being regular, so I don’t see how you could get rid of the assumption

[Josha Dekker]

yes, I think you are right. I guess I'll need to just accept that we repeatedly need that assumption in #11800 (and the follow-up #12087 which I haven't put up for review yet) which is a pity, as it makes some instances impossible (as they would require this assumption).

[Anatole Dedecker]

Is this really an issue ? If so then you could use docs#Fact to make it instance-usable

[Josha Dekker]

Thanks, I'll try that for #12087, I don't think I've had to drop instances in #11800 yet.

[Josha Dekker]

I've done this (= use Fact for instances) for #12087 now, I think that one is ready for review once #11800 merges!