Documentation
QuantumInfo
.
ForMathlib
.
Misc
Search
return to top
source
Imports
Init
Mathlib.LinearAlgebra.BilinearMap
Mathlib.Order.Notation
Mathlib.Tactic.Finiteness
Mathlib.Topology.MetricSpace.Defs
Mathlib.Topology.UniformSpace.Cauchy
Imported by
ite_eq_top
subtype_val_iSup
subtype_val_iSup'
subtype_val_iInf
subtype_val_iInf'
source
theorem
ite_eq_top
{
α
:
Type
u_1}
[
Top
α
]
(
h
:
Prop
)
[
Decidable
h
]
{
x
y
:
α
}
(
hx
:
x
≠
⊤
)
(
hy
:
y
≠
⊤
)
:
(
if
h
then
x
else
y
)
≠
⊤
source
theorem
subtype_val_iSup
{
ι
:
Type
u_1}
{
α
:
Type
u_2}
[
i
:
Nonempty
ι
]
[
ConditionallyCompleteLattice
α
]
{
f
:
ι
→
α
}
{
a
b
:
α
}
[
Fact
(
a
≤
b
)
]
(
h
:
∀ (
i
:
ι
),
f
i
∈
Set.Icc
a
b
)
:
↑
(⨆ (
i
:
ι
),
⟨
f
i
,
⋯
⟩
)
=
⨆ (
i
:
ι
),
f
i
source
theorem
subtype_val_iSup'
{
ι
:
Type
u_1}
{
α
:
Type
u_2}
[
i
:
Nonempty
ι
]
[
ConditionallyCompleteLattice
α
]
{
f
:
ι
→
α
}
{
a
b
:
α
}
[
Fact
(
a
≤
b
)
]
(
h
:
∀ (
i
:
ι
),
f
i
∈
Set.Icc
a
b
)
:
⨆ (
i
:
ι
),
⟨
f
i
,
⋯
⟩
=
⟨
⨆ (
i
:
ι
),
f
i
,
⋯
⟩
source
theorem
subtype_val_iInf
{
ι
:
Type
u_1}
{
α
:
Type
u_2}
[
i
:
Nonempty
ι
]
[
ConditionallyCompleteLattice
α
]
{
f
:
ι
→
α
}
{
a
b
:
α
}
[
Fact
(
a
≤
b
)
]
(
h
:
∀ (
i
:
ι
),
f
i
∈
Set.Icc
a
b
)
:
↑
(⨅ (
i
:
ι
),
⟨
f
i
,
⋯
⟩
)
=
⨅ (
i
:
ι
),
f
i
source
theorem
subtype_val_iInf'
{
ι
:
Type
u_1}
{
α
:
Type
u_2}
[
i
:
Nonempty
ι
]
[
ConditionallyCompleteLattice
α
]
{
f
:
ι
→
α
}
{
a
b
:
α
}
[
Fact
(
a
≤
b
)
]
(
h
:
∀ (
i
:
ι
),
f
i
∈
Set.Icc
a
b
)
:
⨅ (
i
:
ι
),
⟨
f
i
,
⋯
⟩
=
⟨
⨅ (
i
:
ι
),
f
i
,
⋯
⟩