Documentation
Mathlib
.
Algebra
.
Order
.
Group
.
CompleteLattice
Search
Google site search
return to top
source
Imports
Init
Mathlib.Order.ConditionallyCompleteLattice.Basic
Mathlib.Algebra.Order.Group.OrderIso
Imported by
ciSup_add
ciSup_mul
ciSup_sub
ciSup_div
ciInf_add
ciInf_mul
ciInf_sub
ciInf_div
add_ciSup
mul_ciSup
add_ciInf
mul_ciInf
Distributivity of group operations over supremum/infimum
#
source
theorem
ciSup_add
{ι :
Type
u_1}
{G :
Type
u_2}
[
AddGroup
G
]
[
ConditionallyCompleteLattice
G
]
[
Nonempty
ι
]
{f :
ι
→
G
}
[
CovariantClass
G
G
(
Function.swap
fun (
x1
x2
:
G
) =>
x1
+
x2
)
fun (
x1
x2
:
G
) =>
x1
≤
x2
]
(hf :
BddAbove
(
Set.range
f
)
)
(a :
G
)
:
(⨆ (
i
:
ι
),
f
i
)
+
a
=
⨆ (
i
:
ι
),
f
i
+
a
source
theorem
ciSup_mul
{ι :
Type
u_1}
{G :
Type
u_2}
[
Group
G
]
[
ConditionallyCompleteLattice
G
]
[
Nonempty
ι
]
{f :
ι
→
G
}
[
CovariantClass
G
G
(
Function.swap
fun (
x1
x2
:
G
) =>
x1
*
x2
)
fun (
x1
x2
:
G
) =>
x1
≤
x2
]
(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
}
[
CovariantClass
G
G
(
Function.swap
fun (
x1
x2
:
G
) =>
x1
+
x2
)
fun (
x1
x2
:
G
) =>
x1
≤
x2
]
(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
}
[
CovariantClass
G
G
(
Function.swap
fun (
x1
x2
:
G
) =>
x1
*
x2
)
fun (
x1
x2
:
G
) =>
x1
≤
x2
]
(hf :
BddAbove
(
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
}
[
CovariantClass
G
G
(
Function.swap
fun (
x1
x2
:
G
) =>
x1
+
x2
)
fun (
x1
x2
:
G
) =>
x1
≤
x2
]
(hf :
BddBelow
(
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
}
[
CovariantClass
G
G
(
Function.swap
fun (
x1
x2
:
G
) =>
x1
*
x2
)
fun (
x1
x2
:
G
) =>
x1
≤
x2
]
(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
}
[
CovariantClass
G
G
(
Function.swap
fun (
x1
x2
:
G
) =>
x1
+
x2
)
fun (
x1
x2
:
G
) =>
x1
≤
x2
]
(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
}
[
CovariantClass
G
G
(
Function.swap
fun (
x1
x2
:
G
) =>
x1
*
x2
)
fun (
x1
x2
:
G
) =>
x1
≤
x2
]
(hf :
BddBelow
(
Set.range
f
)
)
(a :
G
)
:
(⨅ (
i
:
ι
),
f
i
)
/
a
=
⨅ (
i
:
ι
),
f
i
/
a
source
theorem
add_ciSup
{ι :
Type
u_1}
{G :
Type
u_2}
[
AddGroup
G
]
[
ConditionallyCompleteLattice
G
]
[
Nonempty
ι
]
{f :
ι
→
G
}
[
CovariantClass
G
G
(fun (
x1
x2
:
G
) =>
x1
+
x2
)
fun (
x1
x2
:
G
) =>
x1
≤
x2
]
(hf :
BddAbove
(
Set.range
f
)
)
(a :
G
)
:
a
+
⨆ (
i
:
ι
),
f
i
=
⨆ (
i
:
ι
),
a
+
f
i
source
theorem
mul_ciSup
{ι :
Type
u_1}
{G :
Type
u_2}
[
Group
G
]
[
ConditionallyCompleteLattice
G
]
[
Nonempty
ι
]
{f :
ι
→
G
}
[
CovariantClass
G
G
(fun (
x1
x2
:
G
) =>
x1
*
x2
)
fun (
x1
x2
:
G
) =>
x1
≤
x2
]
(hf :
BddAbove
(
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
}
[
CovariantClass
G
G
(fun (
x1
x2
:
G
) =>
x1
+
x2
)
fun (
x1
x2
:
G
) =>
x1
≤
x2
]
(hf :
BddBelow
(
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
}
[
CovariantClass
G
G
(fun (
x1
x2
:
G
) =>
x1
*
x2
)
fun (
x1
x2
:
G
) =>
x1
≤
x2
]
(hf :
BddBelow
(
Set.range
f
)
)
(a :
G
)
:
a
*
⨅ (
i
:
ι
),
f
i
=
⨅ (
i
:
ι
),
a
*
f
i