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.

ink

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.

ink

instance instBornologyForAll {ι : Type u_1} {π : ι → Type u_2} [inst : Fintype ι] [inst : (i : ι) → Bornology (π i)] : Bornology ((i : ι) → π i)

Equations

• instBornologyForAll = { cobounded' := Filter.coprodᵢ fun i => Bornology.cobounded (π i), le_cofinite' := (_ : (Filter.coprodᵢ fun i => Bornology.cobounded (π i)) ≤ Filter.cofinite) }

ink

def Bornology.induced {α : Type u_1} {β : Type u_2} [inst : Bornology β] (f : α → β) : Bornology α

Inverse image of a bornology.

Equations

• Bornology.induced f = { cobounded' := Filter.comap f (Bornology.cobounded β), le_cofinite' := (_ : Filter.comap f (Bornology.cobounded β) ≤ Filter.cofinite) }

ink

instance instBornologySubtype {α : Type u_1} [inst : Bornology α] {p : α → Prop} : Bornology (Subtype p)

Equations

• instBornologySubtype = Bornology.induced Subtype.val

Bounded sets in α × β× β

ink

theorem Bornology.cobounded_prod {α : Type u_1} {β : Type u_2} [inst : Bornology α] [inst : Bornology β] : Bornology.cobounded (α × β) = Filter.coprod (Bornology.cobounded α) (Bornology.cobounded β)

ink

theorem Bornology.isBounded_image_fst_and_snd {α : Type u_2} {β : Type u_1} [inst : Bornology α] [inst : Bornology β] {s : Set (α × β)} : Bornology.IsBounded (Prod.fst '' s) ∧ Bornology.IsBounded (Prod.snd '' s) ↔ Bornology.IsBounded s

ink

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) : Bornology.IsBounded s

ink

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) : Bornology.IsBounded t

ink

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) : Bornology.IsBounded (s ×ˢ t)

ink

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)) : Bornology.IsBounded (s ×ˢ t) ↔ Bornology.IsBounded s ∧ Bornology.IsBounded t

ink

theorem Bornology.isBounded_prod {α : Type u_2} {β : Type u_1} [inst : Bornology α] [inst : Bornology β] {s : Set α} {t : Set β} : Bornology.IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ Bornology.IsBounded s ∧ Bornology.IsBounded t

ink

theorem Bornology.isBounded_prod_self {α : Type u_1} [inst : Bornology α] {s : Set α} : Bornology.IsBounded (s ×ˢ s) ↔ Bornology.IsBounded s

Bounded sets in Π i, π i

ink

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)

ink

theorem Bornology.forall_isBounded_image_eval_iff {ι : Type u_1} {π : ι → Type u_2} [inst : Fintype ι] [inst : (i : ι) → Bornology (π i)] {s : Set ((i : ι) → π i)} : (∀ (i : ι), Bornology.IsBounded (Function.eval i '' s)) ↔ Bornology.IsBounded s

ink

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)) : Bornology.IsBounded (Set.pi Set.univ S)

ink

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)

ink

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}

ink

theorem Bornology.isBounded_induced {α : Type u_1} {β : Type u_2} [inst : Bornology β] {f : α → β} {s : Set α} : Bornology.IsBounded s ↔ Bornology.IsBounded (f '' s)

ink

theorem Bornology.isBounded_image_subtype_val {α : Type u_1} [inst : Bornology α] {p : α → Prop} {s : Set { x // p x }} : Bornology.IsBounded (Subtype.val '' s) ↔ Bornology.IsBounded s

Bounded spaces

ink

instance instBoundedSpaceProdInstBornologyProd {α : Type u_1} {β : Type u_2} [inst : Bornology α] [inst : Bornology β] [inst : BoundedSpace α] [inst : BoundedSpace β] : BoundedSpace (α × β)

Equations

• @instBoundedSpaceProdInstBornologyProd = @instBoundedSpaceProdInstBornologyProd.proof_1

ink

instance instBoundedSpaceForAllInstBornologyForAll {ι : Type u_1} {π : ι → Type u_2} [inst : Fintype ι] [inst : (i : ι) → Bornology (π i)] [inst : ∀ (i : ι), BoundedSpace (π i)] : BoundedSpace ((i : ι) → π i)

Equations

• @instBoundedSpaceForAllInstBornologyForAll = @instBoundedSpaceForAllInstBornologyForAll.proof_1

ink

theorem boundedSpace_induced_iff {α : Type u_1} {β : Type u_2} [inst : Bornology β] {f : α → β} : BoundedSpace α ↔ Bornology.IsBounded (Set.range f)

ink

theorem boundedSpace_subtype_iff {α : Type u_1} [inst : Bornology α] {p : α → Prop} : BoundedSpace (Subtype p) ↔ Bornology.IsBounded { x | p x }

ink

theorem boundedSpace_val_set_iff {α : Type u_1} [inst : Bornology α] {s : Set α} : BoundedSpace ↑s ↔ Bornology.IsBounded s

ink

theorem Bornology.IsBounded.boundedSpace_subtype {α : Type u_1} [inst : Bornology α] {p : α → Prop} : Bornology.IsBounded { x | p x } → BoundedSpace (Subtype p)

Alias of the reverse direction of boundedSpace_subtype_iff.

ink

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

Alias of the reverse direction of boundedSpace_val_set_iff.

ink

instance instBoundedSpaceSubtypeInstBornologySubtype {α : Type u_1} [inst : Bornology α] [inst : BoundedSpace α] {p : α → Prop} : BoundedSpace (Subtype p)

Equations

• @instBoundedSpaceSubtypeInstBornologySubtype = @instBoundedSpaceSubtypeInstBornologySubtype.proof_1

Additive, Multiplicative

The bornology on those type synonyms is inherited without change.

ink

instance instBornologyAdditive {α : Type u_1} [inst : Bornology α] : Bornology (Additive α)

Equations

• instBornologyAdditive = inst

ink

instance instBornologyMultiplicative {α : Type u_1} [inst : Bornology α] : Bornology (Multiplicative α)

Equations

• instBornologyMultiplicative = inst

ink

instance instBoundedSpaceAdditiveInstBornologyAdditive {α : Type u_1} [inst : Bornology α] [inst : BoundedSpace α] : BoundedSpace (Additive α)

Equations

• @instBoundedSpaceAdditiveInstBornologyAdditive = @instBoundedSpaceAdditiveInstBornologyAdditive.proof_1

ink

instance instBoundedSpaceMultiplicativeInstBornologyMultiplicative {α : Type u_1} [inst : Bornology α] [inst : BoundedSpace α] : BoundedSpace (Multiplicative α)

Equations

• @instBoundedSpaceMultiplicativeInstBornologyMultiplicative = @instBoundedSpaceMultiplicativeInstBornologyMultiplicative.proof_1

Order dual

The bornology on this type synonym is inherited without change.

ink

instance instBornologyOrderDual {α : Type u_1} [inst : Bornology α] : Bornology αᵒᵈ

Equations

• instBornologyOrderDual = inst

ink

instance instBoundedSpaceOrderDualInstBornologyOrderDual {α : Type u_1} [inst : Bornology α] [inst : BoundedSpace α] : BoundedSpace αᵒᵈ

Equations

• @instBoundedSpaceOrderDualInstBornologyOrderDual = @instBoundedSpaceOrderDualInstBornologyOrderDual.proof_1