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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
: