Documentation

Mathlib.Topology.Bornology.Constructions

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 instBornologyProd {α : Type u_1} {β : Type u_2} [inst : Bornology α] [inst : Bornology β] :
Bornology (α × β)
Equations
  • One or more equations did not get rendered due to their size.
instance instBornologyForAll {ι : Type u_1} {π : ιType u_2} [inst : Fintype ι] [inst : (i : ι) → Bornology (π i)] :
Bornology ((i : ι) → π i)
Equations
def Bornology.induced {α : Type u_1} {β : Type u_2} [inst : Bornology β] (f : αβ) :

Inverse image of a bornology.

Equations
instance instBornologySubtype {α : Type u_1} [inst : Bornology α] {p : αProp} :
Equations

Bounded sets in α × β× β #

theorem Bornology.isBounded_image_fst_and_snd {α : Type u_2} {β : Type u_1} [inst : Bornology α] [inst : Bornology β] {s : Set (α × β)} :
theorem Bornology.IsBounded.fst_of_prod {α : Type u_2} {β : Type u_1} [inst : Bornology α] [inst : Bornology β] {s : Set α} {t : Set β} (h : Bornology.IsBounded (s ×ˢ t)) (ht : Set.Nonempty t) :
theorem Bornology.IsBounded.snd_of_prod {α : Type u_2} {β : Type u_1} [inst : Bornology α] [inst : Bornology β] {s : Set α} {t : Set β} (h : Bornology.IsBounded (s ×ˢ t)) (hs : Set.Nonempty s) :
theorem Bornology.IsBounded.prod {α : Type u_1} {β : Type u_2} [inst : Bornology α] [inst : Bornology β] {s : Set α} {t : Set β} (hs : Bornology.IsBounded s) (ht : Bornology.IsBounded t) :
theorem Bornology.isBounded_prod_of_nonempty {α : Type u_2} {β : Type u_1} [inst : Bornology α] [inst : Bornology β] {s : Set α} {t : Set β} (hne : Set.Nonempty (s ×ˢ t)) :
theorem Bornology.isBounded_prod {α : Type u_2} {β : Type u_1} [inst : Bornology α] [inst : Bornology β] {s : Set α} {t : Set β} :

Bounded sets in Π i, π i #

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

Bounded sets in {x // p x} #

theorem Bornology.isBounded_induced {α : Type u_1} {β : Type u_2} [inst : Bornology β] {f : αβ} {s : Set α} :
theorem Bornology.isBounded_image_subtype_val {α : Type u_1} [inst : Bornology α] {p : αProp} {s : Set { x // p x }} :

Bounded spaces #

instance instBoundedSpaceForAllInstBornologyForAll {ι : Type u_1} {π : ιType u_2} [inst : Fintype ι] [inst : (i : ι) → Bornology (π i)] [inst : ∀ (i : ι), BoundedSpace (π i)] :
BoundedSpace ((i : ι) → π i)
Equations
theorem boundedSpace_induced_iff {α : Type u_1} {β : Type u_2} [inst : Bornology β] {f : αβ} :
theorem boundedSpace_subtype_iff {α : Type u_1} [inst : Bornology α] {p : αProp} :
theorem Bornology.IsBounded.boundedSpace_subtype {α : Type u_1} [inst : Bornology α] {p : αProp} :

Alias of the reverse direction of boundedSpace_subtype_iff.

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

Alias of the reverse direction of boundedSpace_val_set_iff.

Additive, Multiplicative #

The bornology on those type synonyms is inherited without change.

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

Order dual #

The bornology on this type synonym is inherited without change.

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