instance
MeasurableSpace.instCountableOrCountablyGeneratedProd_testingLowerBounds
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
[hα : MeasurableSpace.CountableOrCountablyGenerated α γ]
[hβ : MeasurableSpace.CountableOrCountablyGenerated β γ]
:
Equations
- ⋯ = ⋯
theorem
MeasurableSpace.countableOrCountablyGenerated_left_of_prod_left_of_nonempty
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
[Nonempty β]
[h : MeasurableSpace.CountableOrCountablyGenerated (α × β) γ]
:
theorem
MeasurableSpace.countableOrCountablyGenerated_right_of_prod_left_of_nonempty
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
[Nonempty α]
[h : MeasurableSpace.CountableOrCountablyGenerated (α × β) γ]
:
theorem
MeasurableSpace.countablyGenerated_left_of_prod_of_nonempty
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[Nonempty β]
(h : MeasurableSpace.CountablyGenerated (α × β))
:
theorem
MeasurableSpace.countablyGenerated_right_of_prod_of_nonempty
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[Nonempty α]
(h : MeasurableSpace.CountablyGenerated (α × β))
:
theorem
MeasurableSpace.countableOrCountablyGenerated_right_of_prod_right_of_nonempty
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
[Nonempty β]
[h : MeasurableSpace.CountableOrCountablyGenerated α (β × γ)]
:
theorem
MeasurableSpace.countableOrCountablyGenerated_left_of_prod_right_of_nonempty
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
[Nonempty γ]
[h : MeasurableSpace.CountableOrCountablyGenerated α (β × γ)]
:
instance
MeasurableSpace.instCountableOrCountablyGeneratedProd_testingLowerBounds_1
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
[h : MeasurableSpace.CountableOrCountablyGenerated (α × β) γ]
:
Equations
- ⋯ = ⋯
instance
MeasurableSpace.instCountablyGeneratedProd_testingLowerBounds
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace.CountablyGenerated (α × β)]
:
Equations
- ⋯ = ⋯