# mathlib3documentation

topology.bornology.constructions

# 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]
def prod.bornology {α : Type u_1} {β : Type u_2} [bornology α] [bornology β] :
bornology × β)
Equations
@[protected, instance]
def pi.bornology {ι : Type u_3} {π : ι Type u_4} [fintype ι] [Π (i : ι), bornology (π i)] :
bornology (Π (i : ι), π i)
Equations
@[reducible]
def bornology.induced {α : Type u_1} {β : Type u_2} [bornology β] (f : α β) :

Inverse image of a bornology.

Equations
@[protected, instance]
def subtype.bornology {α : Type u_1} [bornology α] {p : α Prop} :
Equations

### Bounded sets in α × β#

theorem bornology.cobounded_prod {α : Type u_1} {β : Type u_2} [bornology α] [bornology β] :
theorem bornology.is_bounded_image_fst_and_snd {α : Type u_1} {β : Type u_2} [bornology α] [bornology β] {s : set × β)} :
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) :
theorem bornology.is_bounded_prod_of_nonempty {α : Type u_1} {β : Type u_2} [bornology α] [bornology β] {s : set α} {t : set β} (hne : (s ×ˢ t).nonempty) :
theorem bornology.is_bounded_prod {α : Type u_1} {β : Type u_2} [bornology α] [bornology β] {s : set α} {t : set β} :
theorem bornology.is_bounded_prod_self {α : Type u_1} [bornology α] {s : set α} :

### 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 : ι),
theorem bornology.is_bounded.pi {ι : Type u_3} {π : ι Type u_4} [fintype ι] [Π (i : ι), bornology (π i)] {S : Π (i : ι), set (π i)} (h : (i : ι), bornology.is_bounded (S i)) :
theorem bornology.is_bounded_pi_of_nonempty {ι : Type u_3} {π : ι Type u_4} [fintype ι] [Π (i : ι), bornology (π i)] {S : Π (i : ι), set (π i)} (hne : (set.univ.pi S).nonempty) :
(i : ι), bornology.is_bounded (S i)
theorem bornology.is_bounded_pi {ι : Type u_3} {π : ι Type u_4} [fintype ι] [Π (i : ι), bornology (π i)] {S : Π (i : ι), set (π i)} :
( (i : ι), S i = ) (i : ι), bornology.is_bounded (S i)

### Bounded sets in {x // p x}#

theorem bornology.is_bounded_induced {α : Type u_1} {β : Type u_2} [bornology β] {f : α β} {s : set α} :
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 β]  :
@[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_induced_iff {α : Type u_1} {β : Type u_2} [bornology β] {f : α β} :
theorem bounded_space_subtype_iff {α : Type u_1} [bornology α] {p : α Prop} :
bornology.is_bounded {x : α | p x}
theorem bounded_space_coe_set_iff {α : Type u_1} [bornology α] {s : set α} :
theorem bornology.is_bounded.bounded_space_subtype {α : Type u_1} [bornology α] {p : α Prop} :
bornology.is_bounded {x : α | p x}

Alias of the reverse direction of bounded_space_subtype_iff.

theorem bornology.is_bounded.bounded_space_coe {α : Type u_1} [bornology α] {s : set α} :

Alias of the reverse direction of bounded_space_coe_set_iff.

@[protected, instance]
def subtype.bounded_space {α : Type u_1} [bornology α] {p : α Prop} :

### additive, multiplicative#

The bornology on those type synonyms is inherited without change.

@[protected, instance]
def additive.bornology {α : Type u_1} [bornology α] :
Equations
@[protected, instance]
def multiplicative.bornology {α : Type u_1} [bornology α] :
Equations
@[protected, instance]
def additive.bounded_space {α : Type u_1} [bornology α]  :
@[protected, instance]
def multiplicative.bounded_space {α : Type u_1} [bornology α]  :

### Order dual #

The bornology on this type synonym is inherited without change.

@[protected, instance]
def order_dual.bornology {α : Type u_1} [bornology α] :
Equations
@[protected, instance]
def order_dual.bounded_space {α : Type u_1} [bornology α]  :