Card. of subset is less than product of card. of proj

Stream: Is there code for X?

[Josha Dekker]

Hi, I want to establish the following, which I have a hard time in doing. Is this in Mathlib under some name that I couldn't find, or is this missing? If the latter, does anyone have any pointers?

import Mathlib.Order.Filter.CardinalInter
import Mathlib.SetTheory.Cardinal.Ordinal
import Mathlib.SetTheory.Cardinal.Cofinality

open Set Filter Cardinal

universe u
variable {ι α β : Type u} {c : Cardinal.{u}} {hreg : Cardinal.IsRegular c} {l : Filter α}
variable {s : Set (α × α)} {h1 : #↑(Prod.fst '' s) < c} {h2 : #↑(Prod.snd '' s) < c}
variable {prod : #(↑(Prod.fst '' s) × ↑(Prod.snd '' s)) < c}

example : #↑s ≤ #(↑(Prod.fst '' s) × ↑(Prod.snd '' s)) := by
  sorry

[Josha Dekker]

Intuitively, sending a point to its projection should be an injective function, but I've not been particularly succesful with that attempt

[Josha Dekker]

I can establish that the function is injective:

example : #↑s ≤ #(↑(Prod.fst '' s) × ↑(Prod.snd '' s)) := by
  let f := fun (p : α × α) => (Prod.fst p, Prod.snd p)
  have hf : Function.Injective f := by
    intro x y hxy
    simp only [Prod.mk.eta, f] at hxy
    exact hxy
  sorry

[Ruben Van de Velde]

import Mathlib.Order.Filter.CardinalInter
import Mathlib.SetTheory.Cardinal.Ordinal
import Mathlib.SetTheory.Cardinal.Cofinality

open Set Filter Cardinal

universe u
variable {ι α β : Type u} {c : Cardinal.{u}} {hreg : Cardinal.IsRegular c} {l : Filter α}
variable {s : Set (α × α)} {h1 : #↑(Prod.fst '' s) < c} {h2 : #↑(Prod.snd '' s) < c}
variable {prod : #(↑(Prod.fst '' s) × ↑(Prod.snd '' s)) < c}

example : #↑s ≤ #(↑(Prod.fst '' s) × ↑(Prod.snd '' s)) := by
  refine mk_le_of_injective
    (f := fun a => ⟨⟨a.1.fst, ?_⟩, ⟨a.1.snd, ?_⟩⟩)
    ?_
  · simp
    use a.1.snd
    simp
  · simp
    use a.1.fst
    simp
  intro x y h
  dsimp only at h
  simp [← Prod.ext_iff] at h
  exact SetCoe.ext h

[Ruben Van de Velde]

Possibly you can write my function as a restriction of your f, but that seems harder than writing out the function you need manually

[Josha Dekker]

Excellent, thank you! Do you think this is worth PR'ing in some form? (I'm just using it as a building block in 1 lemma at the moment)

[Ruben Van de Velde]

I don't know

[Josha Dekker]

Of course some assumptions can be dropped here, I forgot to remove them here...
I've ran into a situation where I wanted this result before, but then I found a (situation-specific) work-around that was shorter than this. In general I guess it may be useful to have? Or some result that establishes that s is a subset of the product in the RHS?