lift_mk_le_lift_mk_mul_of_lift_mk_preimage_le

English

A lifting of the previous bound holds after applying lift to the cardinalities.

Русский

После применения lift к кардинальностям справедливо аналогичное неравенство.

LaTeX

$$$\\forall f,\\, \\forall c,\\; \\operatorname{lift}\\;\\#\\alpha \\le \\operatorname{lift}\\;\\#\\beta \\cdot c$ under appropriate hf$$

Lean4

theorem lift_mk_le_lift_mk_mul_of_lift_mk_preimage_le {α : Type u} {β : Type v} {c : Cardinal} (f : α → β)
    (hf : ∀ b : β, lift.{v} #(f ⁻¹' { b }) ≤ c) : lift.{v} #α ≤ lift.{u} #β * c :=
  (mk_le_mk_mul_of_mk_preimage_le fun x : ULift.{v} α => ULift.up.{u} (f x.1)) <|
    ULift.forall.2 fun b =>
      (mk_congr <|
            (Equiv.ulift.image _).trans
              (Equiv.trans
                (by
                  rw [Equiv.image_eq_preimage]
                  simp only [preimage, mem_singleton_iff, ULift.up_inj, mem_setOf_eq, coe_setOf]
                  exact Equiv.refl _)
                Equiv.ulift.symm)).trans_le
        (hf b)

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