Bornology structure on products and subtypes #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we define bornology and bounded_space instances on α × β, Π i, π i, and
{x // p x}. We also prove basic lemmas about bornology.cobounded and bornology.is_bounded
on these types.
@[protected, instance]
Equations
- prod.bornology = {cobounded := (bornology.cobounded α).coprod (bornology.cobounded β), le_cofinite := _}
@[protected, instance]
Equations
- pi.bornology = {cobounded := filter.Coprod (λ (i : ι), bornology.cobounded (π i)), le_cofinite := _}
@[reducible]
Inverse image of a bornology.
Equations
- bornology.induced f = {cobounded := filter.comap f (bornology.cobounded β), le_cofinite := _}
@[protected, instance]
Equations
Bounded sets in α × β #
theorem
bornology.cobounded_prod
{α : Type u_1}
{β : Type u_2}
[bornology α]
[bornology β] :
bornology.cobounded (α × β) = (bornology.cobounded α).coprod (bornology.cobounded β)
theorem
bornology.is_bounded.fst_of_prod
{α : Type u_1}
{β : Type u_2}
[bornology α]
[bornology β]
{s : set α}
{t : set β}
(h : bornology.is_bounded (s ×ˢ t))
(ht : t.nonempty) :
theorem
bornology.is_bounded.snd_of_prod
{α : Type u_1}
{β : Type u_2}
[bornology α]
[bornology β]
{s : set α}
{t : set β}
(h : bornology.is_bounded (s ×ˢ t))
(hs : s.nonempty) :
theorem
bornology.is_bounded.prod
{α : Type u_1}
{β : Type u_2}
[bornology α]
[bornology β]
{s : set α}
{t : set β}
(hs : bornology.is_bounded s)
(ht : bornology.is_bounded t) :
bornology.is_bounded (s ×ˢ t)
theorem
bornology.is_bounded_prod
{α : Type u_1}
{β : Type u_2}
[bornology α]
[bornology β]
{s : set α}
{t : set β} :
bornology.is_bounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ bornology.is_bounded s ∧ bornology.is_bounded t
theorem
bornology.is_bounded_prod_self
{α : Type u_1}
[bornology α]
{s : set α} :
bornology.is_bounded (s ×ˢ s) ↔ bornology.is_bounded s
Bounded sets in Π i, π i #
theorem
bornology.cobounded_pi
{ι : Type u_3}
{π : ι → Type u_4}
[fintype ι]
[Π (i : ι), bornology (π i)] :
bornology.cobounded (Π (i : ι), π i) = filter.Coprod (λ (i : ι), bornology.cobounded (π i))
theorem
bornology.forall_is_bounded_image_eval_iff
{ι : Type u_3}
{π : ι → Type u_4}
[fintype ι]
[Π (i : ι), bornology (π i)]
{s : set (Π (i : ι), π i)} :
(∀ (i : ι), bornology.is_bounded (function.eval i '' s)) ↔ bornology.is_bounded s
Bounded sets in {x // p x} #
theorem
bornology.is_bounded_induced
{α : Type u_1}
{β : Type u_2}
[bornology β]
{f : α → β}
{s : set α} :
bornology.is_bounded s ↔ bornology.is_bounded (f '' s)
theorem
bornology.is_bounded_image_subtype_coe
{α : Type u_1}
[bornology α]
{p : α → Prop}
{s : set {x // p x}} :
Bounded spaces #
@[protected, instance]
def
prod.bounded_space
{α : Type u_1}
{β : Type u_2}
[bornology α]
[bornology β]
[bounded_space α]
[bounded_space β] :
bounded_space (α × β)
@[protected, instance]
def
pi.bounded_space
{ι : Type u_3}
{π : ι → Type u_4}
[fintype ι]
[Π (i : ι), bornology (π i)]
[∀ (i : ι), bounded_space (π i)] :
bounded_space (Π (i : ι), π i)
theorem
bounded_space_subtype_iff
{α : Type u_1}
[bornology α]
{p : α → Prop} :
bounded_space (subtype p) ↔ bornology.is_bounded {x : α | p x}
theorem
bornology.is_bounded.bounded_space_subtype
{α : Type u_1}
[bornology α]
{p : α → Prop} :
bornology.is_bounded {x : α | p x} → bounded_space (subtype p)
Alias of the reverse direction of bounded_space_subtype_iff.
Alias of the reverse direction of bounded_space_coe_set_iff.
@[protected, instance]
def
subtype.bounded_space
{α : Type u_1}
[bornology α]
[bounded_space α]
{p : α → Prop} :
bounded_space (subtype p)
additive, multiplicative #
The bornology on those type synonyms is inherited without change.
@[protected, instance]
Equations
- additive.bornology = _inst_2
@[protected, instance]
Equations
- multiplicative.bornology = _inst_2
@[protected, instance]
@[protected, instance]
Order dual #
The bornology on this type synonym is inherited without change.
@[protected, instance]
Equations
- order_dual.bornology = _inst_2
@[protected, instance]