lift_card_closure_le_card_term — Mathlib

English

The cardinality of the closure, after lifting, is bounded above by the cardinality of the set of terms in s.

Русский

Кардинал closure_L(s), возведённый в более крупную вселенную, ограничен сверху кардиналом множества термов над s.

LaTeX

$$$$ \operatorname{lift}\,#(\operatorname{closure}_L(s)) \le \#(L.\mathrm{Term}(s)). $$$$

Lean4

theorem lift_card_closure_le_card_term : Cardinal.lift.{max u w} #(closure L s) ≤ #(L.Term s) :=
  by
  rw [← SetLike.coe_sort_coe, coe_closure_eq_range_term_realize]
  rw [← Cardinal.lift_id'.{w, max u w} #(L.Term s)]
  exact Cardinal.mk_range_le_lift

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