English
If α is nonempty and (α × β) → γ is CountableOrCountablyGenerated, then β → γ is CountableOrCountablyGenerated.
Русский
Если α непусто и (α × β) → γ имеет свойство CountableOrCountablyGenerated, то β → γ тоже имеет это свойство.
LaTeX
$$$[\text{Nonempty } \alpha] \;[h : \text{CountableOrCountablyGenerated } (\alpha \times \beta) \gamma] \Rightarrow \text{CountableOrCountablyGenerated } \beta \gamma$$$
Lean4
theorem countableOrCountablyGenerated_right_of_prod_left_of_nonempty [Nonempty α]
[h : CountableOrCountablyGenerated (α × β) γ] : CountableOrCountablyGenerated β γ :=
by
rcases h.countableOrCountablyGenerated with (h | h)
· have := countable_right_of_prod_of_nonempty h
infer_instance
· infer_instance
