countableOrCountablyGenerated_prod_left_swap

English

If (α × β) is CountableOrCountablyGenerated relative to γ, then (β × α) is CountableOrCountablyGenerated relative to γ.

Русский

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

LaTeX

$$$[h : \text{CountableOrCountablyGenerated } (\alpha \times \beta) \gamma] \Rightarrow \text{CountableOrCountablyGenerated } (\beta \times \alpha) \gamma$$$

Lean4

theorem countableOrCountablyGenerated_prod_left_swap [h : CountableOrCountablyGenerated (α × β) γ] :
    CountableOrCountablyGenerated (β × α) γ := by
  rcases h with (h | h)
  · refine ⟨Or.inl countable_prod_swap⟩
  · exact ⟨Or.inr h⟩

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