Distributivity of group operations over supremum/infimum #
theorem
ciSup_mul
{ι : Type u_1}
{G : Type u_2}
[Group G]
[ConditionallyCompleteLattice G]
[Nonempty ι]
{f : ι → G}
[MulRightMono G]
(hf : BddAbove (Set.range f))
(a : G)
:
(⨆ (i : ι), f i) * a = ⨆ (i : ι), f i * a
theorem
ciSup_add
{ι : Type u_1}
{G : Type u_2}
[AddGroup G]
[ConditionallyCompleteLattice G]
[Nonempty ι]
{f : ι → G}
[AddRightMono G]
(hf : BddAbove (Set.range f))
(a : G)
:
(⨆ (i : ι), f i) + a = ⨆ (i : ι), f i + a
theorem
ciSup_div
{ι : Type u_1}
{G : Type u_2}
[Group G]
[ConditionallyCompleteLattice G]
[Nonempty ι]
{f : ι → G}
[MulRightMono G]
(hf : BddAbove (Set.range f))
(a : G)
:
(⨆ (i : ι), f i) / a = ⨆ (i : ι), f i / a
theorem
ciSup_sub
{ι : Type u_1}
{G : Type u_2}
[AddGroup G]
[ConditionallyCompleteLattice G]
[Nonempty ι]
{f : ι → G}
[AddRightMono G]
(hf : BddAbove (Set.range f))
(a : G)
:
(⨆ (i : ι), f i) - a = ⨆ (i : ι), f i - a
theorem
ciInf_mul
{ι : Type u_1}
{G : Type u_2}
[Group G]
[ConditionallyCompleteLattice G]
[Nonempty ι]
{f : ι → G}
[MulRightMono G]
(hf : BddBelow (Set.range f))
(a : G)
:
(⨅ (i : ι), f i) * a = ⨅ (i : ι), f i * a
theorem
ciInf_add
{ι : Type u_1}
{G : Type u_2}
[AddGroup G]
[ConditionallyCompleteLattice G]
[Nonempty ι]
{f : ι → G}
[AddRightMono G]
(hf : BddBelow (Set.range f))
(a : G)
:
(⨅ (i : ι), f i) + a = ⨅ (i : ι), f i + a
theorem
ciInf_div
{ι : Type u_1}
{G : Type u_2}
[Group G]
[ConditionallyCompleteLattice G]
[Nonempty ι]
{f : ι → G}
[MulRightMono G]
(hf : BddBelow (Set.range f))
(a : G)
:
(⨅ (i : ι), f i) / a = ⨅ (i : ι), f i / a
theorem
ciInf_sub
{ι : Type u_1}
{G : Type u_2}
[AddGroup G]
[ConditionallyCompleteLattice G]
[Nonempty ι]
{f : ι → G}
[AddRightMono G]
(hf : BddBelow (Set.range f))
(a : G)
:
(⨅ (i : ι), f i) - a = ⨅ (i : ι), f i - a
theorem
mul_ciSup
{ι : Type u_1}
{G : Type u_2}
[Group G]
[ConditionallyCompleteLattice G]
[Nonempty ι]
{f : ι → G}
[MulLeftMono G]
(hf : BddAbove (Set.range f))
(a : G)
:
a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
theorem
add_ciSup
{ι : Type u_1}
{G : Type u_2}
[AddGroup G]
[ConditionallyCompleteLattice G]
[Nonempty ι]
{f : ι → G}
[AddLeftMono G]
(hf : BddAbove (Set.range f))
(a : G)
:
a + ⨆ (i : ι), f i = ⨆ (i : ι), a + f i
theorem
mul_ciInf
{ι : Type u_1}
{G : Type u_2}
[Group G]
[ConditionallyCompleteLattice G]
[Nonempty ι]
{f : ι → G}
[MulLeftMono G]
(hf : BddBelow (Set.range f))
(a : G)
:
a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i
theorem
add_ciInf
{ι : Type u_1}
{G : Type u_2}
[AddGroup G]
[ConditionallyCompleteLattice G]
[Nonempty ι]
{f : ι → G}
[AddLeftMono G]
(hf : BddBelow (Set.range f))
(a : G)
:
a + ⨅ (i : ι), f i = ⨅ (i : ι), a + f i