Some missing Cardinality API

Stream: mathlib4

[Josha Dekker]

Hi, I've noticed that a few results for (regular) cardinals seem to be missing that I needed for #11758. I've added them in the file where I needed them for now, but I feel that there must be a better place for them. They are analogous results to some results in Data/Set/Countable, but we do not have a dedicated file for Cardinal for these purposes, as far as I could tell. Should I store them in SetTheory/Cardinal/Cofinality for now? (As they require Regular cardinals?)

If there's interest I could set up some more API for regular cardinals (just the usual iUnion/sUnion/bUnion stuff). In this case, would we like a separate file like Data/Set/Countable, or should I place it in SetTheory/Cardinal/Cofinality as well?

import Mathlib.Order.Filter.Basic
import Mathlib.Order.Filter.CountableInter
import Mathlib.SetTheory.Cardinal.Ordinal
import Mathlib.SetTheory.Cardinal.Cofinality

open Set Filter Cardinal

universe u
variable {ι : Type u} {α : Type u} {c : Cardinal.{u}}

-- Some cardinality related lemmas that I needed
def fin_from_regular (hreg : Cardinal.IsRegular c) (n : ℕ) : n < c:= by
  apply lt_of_lt_of_le (nat_lt_aleph0 n) (Cardinal.IsRegular.aleph0_le hreg)

@[simp]
theorem cardinal_iUnion_iff {hι : #ι < c} {hreg : Cardinal.IsRegular c}  {t : ι → Set α} :
    #(⋃ i, t i) < c ↔ ∀ i, #(t i) < c := by
  constructor
  · exact fun h _ =>  lt_of_le_of_lt (Cardinal.mk_le_mk_of_subset <| subset_iUnion _ _) h
  · intro h
    apply lt_of_le_of_lt (Cardinal.mk_sUnion_le _)
    apply Cardinal.mul_lt_of_lt (Cardinal.IsRegular.aleph0_le hreg)
    · exact lt_of_le_of_lt Cardinal.mk_range_le hι
    · apply Cardinal.iSup_lt_of_isRegular hreg
      apply lt_of_le_of_lt Cardinal.mk_range_le hι
      simpa

theorem Cardinal.biUnion_iff {s : Set α} {t : ∀ a ∈ s, Set β} {hreg : Cardinal.IsRegular c}
    (hs : #s < c) : #(⋃ a ∈ s, t a ‹_›) < c ↔ ∀ a (ha : a ∈ s), # (t a ha) < c := by
  rw [biUnion_eq_iUnion, cardinal_iUnion_iff, SetCoe.forall']
  · exact hs
  · exact hreg

[Josha Dekker]

(deleted)

[Ruben Van de Velde]

Btw, you can use #find_home Cardinal.biUnion_iff to see where it might fit (or #find_home!)

[Josha Dekker]

Oops, I forgot that was the use-case for that one. It looks like I guessed the right directory!

[Josha Dekker]

I've moved the auxiliary ones to SetTheory/Cardinal/Cofinality in my PR and modified their style to match that one. I can add more API in the future if that is preferred.