sigma_of_right — Mathlib

English

If β(a) is infinite for some a, then the product (a, β(a)) is infinite.

Русский

Если β(a) бесконечно для данного a, то произведение (a, β(a)) бесконечно.

LaTeX

$$$\\forall β:\\alpha \\to Type*,\\forall a,\\operatorname{Infinite}(β a)\\Rightarrow \\operatorname{Infinite}((a:\\alpha) \\times β a)$$$

Lean4

theorem sigma_of_right {β : α → Type*} {a : α} [Infinite (β a)] : Infinite ((a : α) × β a) :=
  Infinite.of_injective (f := fun x ↦ ⟨a, x⟩) fun _ _ ↦ by simp

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