countableOrCountablyGenerated_left_of_prod_left_of_nonempty

English

If β is nonempty and (α × β) → γ is CountableOrCountablyGenerated, then α → γ is CountableOrCountablyGenerated.

Русский

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

LaTeX

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

Lean4

theorem countableOrCountablyGenerated_left_of_prod_left_of_nonempty [Nonempty β]
    [h : CountableOrCountablyGenerated (α × β) γ] : CountableOrCountablyGenerated α γ :=
  by
  rcases h.countableOrCountablyGenerated with (h | h)
  · have := countable_left_of_prod_of_nonempty h
    infer_instance
  · infer_instance

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