English
The cardinality of the Ore localization is bounded by the maximum of the lifted cardinalities of S and X: #(OreLocalization S X) ≤ max(lift #S, lift #X).
Русский
Кардинал локализации Оре не превышает максимум подъёмов кардиналов S и X.
LaTeX
$$$\\#(OreLocalization S X) \\le \\max(\\mathrm{lift}\\#S, \\mathrm{lift}\\#X)$$$
Lean4
@[to_additive]
theorem cardinalMk_le_max : #(OreLocalization S X) ≤ max (lift.{v} #S) (lift.{u} #X) :=
by
rcases finite_or_infinite X with _ | _
· have := lift_mk_le_lift_mk_of_surjective (oreDiv_one_surjective_of_finite_right S X)
rw [lift_umax.{v, u}, lift_id'] at this
exact le_max_of_le_right this
rcases finite_or_infinite S with _ | _
· have := lift_mk_le_lift_mk_of_surjective (oreDiv_one_surjective_of_finite_left S X)
rw [lift_umax.{v, u}, lift_id'] at this
exact le_max_of_le_right this
convert ← mk_le_of_surjective (show Surjective fun x : X × S ↦ x.1 /ₒ x.2 from Quotient.mk''_surjective)
rw [mk_prod, mul_comm]
refine mul_eq_max ?_ ?_ <;> simp
