Documentation
Mathlib
.
Algebra
.
Order
.
Group
.
CompleteLattice
Search
return to top
source
Imports
Init
Mathlib.Order.ConditionallyCompleteLattice.Indexed
Mathlib.Algebra.Order.Group.OrderIso
Imported by
ciSup_mul
ciSup_add
ciSup_div
ciSup_sub
ciInf_mul
ciInf_add
ciInf_div
ciInf_sub
mul_ciSup
add_ciSup
mul_ciInf
add_ciInf
Distributivity of group operations over supremum/infimum
#
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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