# 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.

instance Prod.instBornology {α : Type u_1} {β : Type u_2} [] [] :
Bornology (α × β)
Equations
• Prod.instBornology = { cobounded' := .coprod , le_cofinite' := }
instance Pi.instBornology {ι : Type u_3} {π : ιType u_4} [(i : ι) → Bornology (π i)] :
Bornology ((i : ι) → π i)
Equations
@[reducible, inline]
abbrev Bornology.induced {α : Type u_5} {β : Type u_6} [] (f : αβ) :

Inverse image of a bornology.

Equations
• = { cobounded' := , le_cofinite' := }
Instances For
instance instBornologySubtype {α : Type u_1} [] {p : αProp} :
Equations

### Bounded sets in α × β#

theorem Bornology.cobounded_prod {α : Type u_1} {β : Type u_2} [] [] :
Bornology.cobounded (α × β) = .coprod
theorem Bornology.isBounded_image_fst_and_snd {α : Type u_1} {β : Type u_2} [] [] {s : Set (α × β)} :
Bornology.IsBounded (Prod.fst '' s) Bornology.IsBounded (Prod.snd '' s)
theorem Bornology.IsBounded.image_fst {α : Type u_1} {β : Type u_2} [] [] {s : Set (α × β)} (hs : ) :
Bornology.IsBounded (Prod.fst '' s)
theorem Bornology.IsBounded.image_snd {α : Type u_1} {β : Type u_2} [] [] {s : Set (α × β)} (hs : ) :
Bornology.IsBounded (Prod.snd '' s)
theorem Bornology.IsBounded.fst_of_prod {α : Type u_1} {β : Type u_2} [] [] {s : Set α} {t : Set β} (h : Bornology.IsBounded (s ×ˢ t)) (ht : t.Nonempty) :
theorem Bornology.IsBounded.snd_of_prod {α : Type u_1} {β : Type u_2} [] [] {s : Set α} {t : Set β} (h : Bornology.IsBounded (s ×ˢ t)) (hs : s.Nonempty) :
theorem Bornology.IsBounded.prod {α : Type u_1} {β : Type u_2} [] [] {s : Set α} {t : Set β} (hs : ) (ht : ) :
theorem Bornology.isBounded_prod_of_nonempty {α : Type u_1} {β : Type u_2} [] [] {s : Set α} {t : Set β} (hne : (s ×ˢ t).Nonempty) :
theorem Bornology.isBounded_prod {α : Type u_1} {β : Type u_2} [] [] {s : Set α} {t : Set β} :
theorem Bornology.isBounded_prod_self {α : Type u_1} [] {s : Set α} :

### Bounded sets in Π i, π i#

theorem Bornology.cobounded_pi {ι : Type u_3} {π : ιType u_4} [(i : ι) → Bornology (π i)] :
Bornology.cobounded ((i : ι) → π i) = Filter.coprodᵢ fun (i : ι) => Bornology.cobounded (π i)
theorem Bornology.forall_isBounded_image_eval_iff {ι : Type u_3} {π : ιType u_4} [(i : ι) → Bornology (π i)] {s : Set ((i : ι) → π i)} :
(∀ (i : ι), )
theorem Bornology.IsBounded.image_eval {ι : Type u_3} {π : ιType u_4} [(i : ι) → Bornology (π i)] {s : Set ((i : ι) → π i)} (hs : ) (i : ι) :
theorem Bornology.IsBounded.pi {ι : Type u_3} {π : ιType u_4} [(i : ι) → Bornology (π i)] {S : (i : ι) → Set (π i)} (h : ∀ (i : ι), Bornology.IsBounded (S i)) :
Bornology.IsBounded (Set.univ.pi S)
theorem Bornology.isBounded_pi_of_nonempty {ι : Type u_3} {π : ιType u_4} [(i : ι) → Bornology (π i)] {S : (i : ι) → Set (π i)} (hne : (Set.univ.pi S).Nonempty) :
Bornology.IsBounded (Set.univ.pi S) ∀ (i : ι), Bornology.IsBounded (S i)
theorem Bornology.isBounded_pi {ι : Type u_3} {π : ιType u_4} [(i : ι) → Bornology (π i)] {S : (i : ι) → Set (π i)} :
Bornology.IsBounded (Set.univ.pi S) (∃ (i : ι), S i = ) ∀ (i : ι), Bornology.IsBounded (S i)

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

theorem Bornology.isBounded_induced {α : Type u_5} {β : Type u_6} [] {f : αβ} {s : Set α} :
theorem Bornology.isBounded_image_subtype_val {α : Type u_1} [] {p : αProp} {s : Set { x : α // p x }} :
Bornology.IsBounded (Subtype.val '' s)

### Bounded spaces #

instance instBoundedSpaceProd {α : Type u_1} {β : Type u_2} [] [] [] [] :
Equations
• =
instance instBoundedSpaceForall {ι : Type u_3} {π : ιType u_4} [(i : ι) → Bornology (π i)] [∀ (i : ι), BoundedSpace (π i)] :
BoundedSpace ((i : ι) → π i)
Equations
• =
theorem boundedSpace_induced_iff {α : Type u_5} {β : Type u_6} [] {f : αβ} :
theorem boundedSpace_subtype_iff {α : Type u_1} [] {p : αProp} :
Bornology.IsBounded {x : α | p x}
theorem boundedSpace_val_set_iff {α : Type u_1} [] {s : Set α} :
theorem Bornology.IsBounded.boundedSpace_subtype {α : Type u_1} [] {p : αProp} :
Bornology.IsBounded {x : α | p x}

Alias of the reverse direction of boundedSpace_subtype_iff.

theorem Bornology.IsBounded.boundedSpace_val {α : Type u_1} [] {s : Set α} :

Alias of the reverse direction of boundedSpace_val_set_iff.

instance instBoundedSpaceSubtype {α : Type u_1} [] [] {p : αProp} :
Equations
• =

### Additive, Multiplicative#

The bornology on those type synonyms is inherited without change.

instance instBornologyAdditive {α : Type u_1} [] :
Equations
instance instBornologyMultiplicative {α : Type u_1} [] :
Equations
• instBornologyMultiplicative = inst
instance instBoundedSpaceAdditive {α : Type u_1} [] [] :
Equations
• = inst
instance instBoundedSpaceMultiplicative {α : Type u_1} [] [] :
Equations
• = inst

### Order dual #

The bornology on this type synonym is inherited without change.

instance instBornologyOrderDual {α : Type u_1} [] :
Equations
• instBornologyOrderDual = inst
instance instBoundedSpaceOrderDual {α : Type u_1} [] [] :
Equations
• = inst