instCountableOrCountablyGeneratedProd

English

If α and β are each CountableOrCountablyGenerated relative to γ, then their product α × β is CountableOrCountablyGenerated relative to γ.

Русский

Если пары типов (α, γ) и (β, γ) обладают свойством CountableOrCountablyGenerated, то произведение α × β имеет это же свойство относительно γ.

LaTeX

$$$\text{CountableOrCountablyGenerated } (\alpha, \beta) \gamma\; \text{ holds if }\; \text{CountableOrCountablyGenerated } \alpha \gamma \text{ and } \text{CountableOrCountablyGenerated } \beta \gamma.$$$

Lean4

instance [hα : CountableOrCountablyGenerated α γ] [hβ : CountableOrCountablyGenerated β γ] :
    CountableOrCountablyGenerated (α × β) γ := by
  rcases hα with (hα | hα) <;> rcases hβ with (hβ | hβ) <;> infer_instance

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