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