Documentation

Mathlib.Algebra.Order.Group.CompleteLattice

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) :
Eq (HMul.hMul (iSup fun (i : ι) => f i) a) (iSup fun (i : ι) => HMul.hMul (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) :
Eq (HAdd.hAdd (iSup fun (i : ι) => f i) a) (iSup fun (i : ι) => HAdd.hAdd (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) :
Eq (HDiv.hDiv (iSup fun (i : ι) => f i) a) (iSup fun (i : ι) => HDiv.hDiv (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) :
Eq (HSub.hSub (iSup fun (i : ι) => f i) a) (iSup fun (i : ι) => HSub.hSub (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) :
Eq (HMul.hMul (iInf fun (i : ι) => f i) a) (iInf fun (i : ι) => HMul.hMul (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) :
Eq (HAdd.hAdd (iInf fun (i : ι) => f i) a) (iInf fun (i : ι) => HAdd.hAdd (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) :
Eq (HDiv.hDiv (iInf fun (i : ι) => f i) a) (iInf fun (i : ι) => HDiv.hDiv (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) :
Eq (HSub.hSub (iInf fun (i : ι) => f i) a) (iInf fun (i : ι) => HSub.hSub (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) :
Eq (HMul.hMul a (iSup fun (i : ι) => f i)) (iSup fun (i : ι) => HMul.hMul 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) :
Eq (HAdd.hAdd a (iSup fun (i : ι) => f i)) (iSup fun (i : ι) => HAdd.hAdd 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) :
Eq (HMul.hMul a (iInf fun (i : ι) => f i)) (iInf fun (i : ι) => HMul.hMul 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) :
Eq (HAdd.hAdd a (iInf fun (i : ι) => f i)) (iInf fun (i : ι) => HAdd.hAdd a (f i))