mk_preimage_down — Mathlib

English

Same bound as before: the family of subsets t ⊆ s with |t| ≤ c has cardinal ≤ max|s| ℵ0^c.

Русский

Та же граница: множество подмножеств t ⊆ s с |t| ≤ c имеет кардинальность ≤ max|s| ℵ0^c.

LaTeX

$$$\\#\\{ t : \\mathcal{P}(s) \\;|\\; \\#t \\le c \\} \\le \\max\\{\\#s, \\aleph_{0}\\}^{\\,c}$$$

Lean4

@[simp]
theorem mk_preimage_down {s : Set α} : #(ULift.down.{v} ⁻¹' s) = lift.{v} (#s) :=
  by
  rw [← mk_uLift, Cardinal.eq]
  constructor
  let f : ULift.down ⁻¹' s → ULift s := fun x ↦ ULift.up (restrictPreimage s ULift.down x)
  have : Function.Bijective f := ULift.up_bijective.comp (restrictPreimage_bijective _ (ULift.down_bijective))
  exact Equiv.ofBijective f this

Похожие утверждения