Bornology structure on products and subtypes #
In this file we define Bornology
and BoundedSpace
instances on α × β
, Π i, π i
, and
{x // p x}
. We also prove basic lemmas about Bornology.cobounded
and Bornology.IsBounded
on these types.
Bounded sets in α × β
#
Bounded sets in Π i, π i
#
theorem
Bornology.IsBounded.image_eval
{ι : Type u_3}
{π : ι → Type u_4}
[(i : ι) → Bornology (π i)]
{s : Set ((i : ι) → π i)}
(hs : IsBounded s)
(i : ι)
:
IsBounded (Function.eval i '' s)
Bounded sets in {x // p x}
#
Bounded spaces #
instance
instBoundedSpaceProd
{α : Type u_1}
{β : Type u_2}
[Bornology α]
[Bornology β]
[BoundedSpace α]
[BoundedSpace β]
:
BoundedSpace (α × β)
instance
instBoundedSpaceForall
{ι : Type u_3}
{π : ι → Type u_4}
[(i : ι) → Bornology (π i)]
[∀ (i : ι), BoundedSpace (π i)]
:
BoundedSpace ((i : ι) → π i)
Alias of the reverse direction of boundedSpace_subtype_iff
.
theorem
Bornology.IsBounded.boundedSpace_val
{α : Type u_1}
[Bornology α]
{s : Set α}
:
IsBounded s → BoundedSpace ↑s
Alias of the reverse direction of boundedSpace_val_set_iff
.
instance
instBoundedSpaceSubtype
{α : Type u_1}
[Bornology α]
[BoundedSpace α]
{p : α → Prop}
:
BoundedSpace (Subtype p)
Additive
, Multiplicative
#
The bornology on those type synonyms is inherited without change.
Equations
instance
instBoundedSpaceAdditive
{α : Type u_1}
[Bornology α]
[BoundedSpace α]
:
BoundedSpace (Additive α)
Order dual #
The bornology on this type synonym is inherited without change.