mathlib documentation

topology.bornology.constructions

Bornology structure on products and subtypes #

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.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 β} :

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)} :
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) :
theorem bornology.is_bounded_pi {ι : Type u_3} {π : ι → Type u_4} [fintype ι] [Π (i : ι), bornology (π i)] {S : Π (i : ι), set (π i)} :
bornology.is_bounded (set.univ.pi S) (∃ (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 β] [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_induced_iff {α : Type u_1} {β : Type u_2} [bornology β] {f : α → β} :
theorem bounded_space_subtype_iff {α : Type u_1} [bornology α] {p : α → Prop} :
theorem bornology.is_bounded.bounded_space_subtype {α : Type u_1} [bornology α] {p : α → Prop} :

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} :

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 α] [bounded_space α] :
@[protected, instance]

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]