Mathlib.Topology.Bornology.Constructions

Prod.instBornology instance

: Bornology (α × β)

Full source

instance Prod.instBornology : Bornology (α × β) where
  cobounded' := (cobounded α).coprod (cobounded β)
  le_cofinite' :=
    @coprod_cofinite α β ▸ coprod_mono ‹Bornology α›.le_cofinite ‹Bornology β›.le_cofinite

Bornology Structure on Product Types

Informal description

For any types $\alpha$ and $\beta$ equipped with bornology structures, the product type $\alpha \times \beta$ inherits a bornology structure where a set is bounded if its projections to both $\alpha$ and $\beta$ are bounded.

Pi.instBornology instance

: Bornology (∀ i, π i)

Full source

instance Pi.instBornology : Bornology (∀ i, π i) where
  cobounded' := Filter.coprodᵢ fun i => cobounded (π i)
  le_cofinite' := iSup_le fun _ ↦ (comap_mono (Bornology.le_cofinite _)).trans (comap_cofinite_le _)

Bornology on Product Types

Informal description

For any family of types $\pi_i$ indexed by $i$, the product type $\forall i, \pi_i$ is equipped with a bornology structure where a set is bounded if and only if its projection to each $\pi_i$ is bounded.

Bornology.induced abbrev

{α β : Type*} [Bornology β] (f : α → β) : Bornology α

Full source

/-- Inverse image of a bornology. -/
abbrev Bornology.induced {α β : Type*} [Bornology β] (f : α → β) : Bornology α where
  cobounded' := comap f (cobounded β)
  le_cofinite' := (comap_mono (Bornology.le_cofinite β)).trans (comap_cofinite_le _)

Induced Bornology via a Function

Informal description

Given a function $f \colon \alpha \to \beta$ where $\beta$ is equipped with a bornology, the *induced bornology* on $\alpha$ is the bornology where a set $S \subseteq \alpha$ is bounded if and only if its image $f(S)$ is bounded in $\beta$.

instBornologySubtype instance

{p : α → Prop} : Bornology (Subtype p)

Full source

instance {p : α → Prop} : Bornology (Subtype p) :=
  Bornology.induced (Subtype.val : Subtype p → α)

Bornology on Subtypes

Informal description

For any type $\alpha$ and predicate $p$ on $\alpha$, the subtype $\{x \mid p x\}$ inherits a bornology structure from $\alpha$, where a set is bounded if and only if its image under the inclusion map is bounded in $\alpha$.

Bornology.cobounded_prod theorem

: cobounded (α × β) = (cobounded α).coprod (cobounded β)

Full source

theorem cobounded_prod : cobounded (α × β) = (cobounded α).coprod (cobounded β) :=
  rfl

Cobounded Filter on Product Space as Coproduct of Factors' Cobounded Filters

Informal description

For any types $\alpha$ and $\beta$ equipped with bornologies, the cobounded filter on the product type $\alpha \times \beta$ is equal to the coproduct of the cobounded filters on $\alpha$ and $\beta$. In other words, $\text{cobounded}(\alpha \times \beta) = \text{cobounded}(\alpha) \sqcup \text{cobounded}(\beta)$.

Bornology.isBounded_image_fst_and_snd theorem

{s : Set (α × β)} : IsBounded (Prod.fst '' s) ∧ IsBounded (Prod.snd '' s) ↔ IsBounded s

Full source

theorem isBounded_image_fst_and_snd {s : Set (α × β)} :
    IsBoundedIsBounded (Prod.fst '' s) ∧ IsBounded (Prod.snd '' s)IsBounded (Prod.fst '' s) ∧ IsBounded (Prod.snd '' s) ↔ IsBounded s :=
  compl_mem_coprod.symm

Boundedness in Product Space via Projections

Informal description

For any subset $s$ of the product space $\alpha \times \beta$, the set $s$ is bounded if and only if both its projections to $\alpha$ (via the first coordinate) and to $\beta$ (via the second coordinate) are bounded. In other words, $s$ is bounded if and only if $\text{IsBounded}(\text{fst}'' s) \land \text{IsBounded}(\text{snd}'' s)$.

Bornology.IsBounded.image_fst theorem

{s : Set (α × β)} (hs : IsBounded s) : IsBounded (Prod.fst '' s)

Full source

lemma IsBounded.image_fst {s : Set (α × β)} (hs : IsBounded s) : IsBounded (Prod.fstProd.fst '' s) :=
  (isBounded_image_fst_and_snd.2 hs).1

Boundedness of First Projection in Product Space

Informal description

For any subset $s$ of the product space $\alpha \times \beta$, if $s$ is bounded, then its projection to $\alpha$ (via the first coordinate) is also bounded. In other words, if $\text{IsBounded}(s)$, then $\text{IsBounded}(\text{fst}'' s)$.

Bornology.IsBounded.image_snd theorem

{s : Set (α × β)} (hs : IsBounded s) : IsBounded (Prod.snd '' s)

Full source

lemma IsBounded.image_snd {s : Set (α × β)} (hs : IsBounded s) : IsBounded (Prod.sndProd.snd '' s) :=
  (isBounded_image_fst_and_snd.2 hs).2

Boundedness of Second Projection in Product Space

Informal description

For any subset $s$ of the product space $\alpha \times \beta$, if $s$ is bounded, then its projection to $\beta$ via the second coordinate is also bounded. In other words, if $\text{IsBounded}(s)$, then $\text{IsBounded}(\text{snd}'' s)$.

Bornology.IsBounded.fst_of_prod theorem

(h : IsBounded (s ×ˢ t)) (ht : t.Nonempty) : IsBounded s

Full source

theorem IsBounded.fst_of_prod (h : IsBounded (s ×ˢ t)) (ht : t.Nonempty) : IsBounded s :=
  fst_image_prod s ht ▸ h.image_fst

Boundedness of First Factor in Nonempty Product

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, if the Cartesian product $s \times t$ is bounded and $t$ is nonempty, then $s$ is bounded.

Bornology.IsBounded.snd_of_prod theorem

(h : IsBounded (s ×ˢ t)) (hs : s.Nonempty) : IsBounded t

Full source

theorem IsBounded.snd_of_prod (h : IsBounded (s ×ˢ t)) (hs : s.Nonempty) : IsBounded t :=
  snd_image_prod hs t ▸ h.image_snd

Boundedness of Second Factor in Nonempty Product of Bounded Sets

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, if the Cartesian product $s \times t$ is bounded and $s$ is nonempty, then $t$ is bounded.

Bornology.IsBounded.prod theorem

(hs : IsBounded s) (ht : IsBounded t) : IsBounded (s ×ˢ t)

Full source

theorem IsBounded.prod (hs : IsBounded s) (ht : IsBounded t) : IsBounded (s ×ˢ t) :=
  isBounded_image_fst_and_snd.1
    ⟨hs.subset <| fst_image_prod_subset _ _, ht.subset <| snd_image_prod_subset _ _⟩

Boundedness of Cartesian Product of Bounded Sets

Informal description

For any bounded sets $s \subseteq \alpha$ and $t \subseteq \beta$, their Cartesian product $s \times t$ is also bounded.

Bornology.isBounded_prod_of_nonempty theorem

(hne : Set.Nonempty (s ×ˢ t)) : IsBounded (s ×ˢ t) ↔ IsBounded s ∧ IsBounded t

Full source

theorem isBounded_prod_of_nonempty (hne : Set.Nonempty (s ×ˢ t)) :
    IsBoundedIsBounded (s ×ˢ t) ↔ IsBounded s ∧ IsBounded t :=
  ⟨fun h => ⟨h.fst_of_prod hne.snd, h.snd_of_prod hne.fst⟩, fun h => h.1.prod h.2⟩

Boundedness of Nonempty Product Sets: $s \times t$ is bounded iff $s$ and $t$ are bounded

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, if their Cartesian product $s \times t$ is nonempty, then $s \times t$ is bounded if and only if both $s$ and $t$ are bounded.

Bornology.isBounded_prod theorem

: IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t

Full source

theorem isBounded_prod : IsBoundedIsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t := by
  rcases s.eq_empty_or_nonempty with (rfl | hs); · simp
  rcases t.eq_empty_or_nonempty with (rfl | ht); · simp
  simp only [hs.ne_empty, ht.ne_empty, isBounded_prod_of_nonempty (hs.prod ht), false_or]

Boundedness of Cartesian Product: $s \times t$ is bounded iff $s$ or $t$ is empty or both are bounded

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the Cartesian product $s \times t$ is bounded if and only if either $s$ is empty, $t$ is empty, or both $s$ and $t$ are bounded.

Bornology.isBounded_prod_self theorem

: IsBounded (s ×ˢ s) ↔ IsBounded s

Full source

theorem isBounded_prod_self : IsBoundedIsBounded (s ×ˢ s) ↔ IsBounded s := by
  rcases s.eq_empty_or_nonempty with (rfl | hs); · simp
  exact (isBounded_prod_of_nonempty (hs.prod hs)).trans and_self_iff

Boundedness of Self-Product Set: $s \times s$ is bounded iff $s$ is bounded

Informal description

For any set $s$ in a bornology space, the Cartesian product $s \times s$ is bounded if and only if $s$ itself is bounded.

Bornology.cobounded_pi theorem

: cobounded (∀ i, π i) = Filter.coprodᵢ fun i => cobounded (π i)

Full source

theorem cobounded_pi : cobounded (∀ i, π i) = Filter.coprodᵢ fun i => cobounded (π i) :=
  rfl

Cobounded Filter on Product Type as Coproduct of Component Filters

Informal description

The cobounded filter on the product type $\forall i, \pi_i$ is equal to the coproduct filter of the cobounded filters on each component $\pi_i$. In other words, \[ \text{cobounded}(\forall i, \pi_i) = \prod_{i} \text{cobounded}(\pi_i). \]

Bornology.forall_isBounded_image_eval_iff theorem

{s : Set (∀ i, π i)} : (∀ i, IsBounded (eval i '' s)) ↔ IsBounded s

Full source

theorem forall_isBounded_image_eval_iff {s : Set (∀ i, π i)} :
    (∀ i, IsBounded (eval i '' s)) ↔ IsBounded s :=
  compl_mem_coprodᵢ.symm

Boundedness in Product Space via Componentwise Boundedness

Informal description

For any set $s$ in the product type $\prod_{i} \pi_i$, the set $s$ is bounded if and only if for every index $i$, the image of $s$ under the evaluation map at $i$ (i.e., $\{f(i) | f \in s\}$) is bounded in $\pi_i$.

Bornology.IsBounded.image_eval theorem

{s : Set (∀ i, π i)} (hs : IsBounded s) (i : ι) : IsBounded (eval i '' s)

Full source

lemma IsBounded.image_eval {s : Set (∀ i, π i)} (hs : IsBounded s) (i : ι) :
    IsBounded (evaleval i '' s) :=
  forall_isBounded_image_eval_iff.2 hs i

Boundedness of Evaluation Images in Product Spaces

Informal description

For any bounded set $s$ in the product space $\prod_{i} \pi_i$ and any index $i$, the image of $s$ under the evaluation map at $i$ (i.e., $\{f(i) \mid f \in s\}$) is bounded in $\pi_i$.

Bornology.IsBounded.pi theorem

(h : ∀ i, IsBounded (S i)) : IsBounded (pi univ S)

Full source

theorem IsBounded.pi (h : ∀ i, IsBounded (S i)) : IsBounded (pi univ S) :=
  forall_isBounded_image_eval_iff.1 fun i => (h i).subset eval_image_univ_pi_subset

Boundedness of Product Sets via Componentwise Boundedness

Informal description

For any family of sets $S_i \subseteq \pi_i$ indexed by $i \in \iota$, if each $S_i$ is bounded in its respective space $\pi_i$, then the product set $\prod_{i \in \iota} S_i$ is bounded in the product space $\prod_{i} \pi_i$.

Bornology.isBounded_pi_of_nonempty theorem

(hne : (pi univ S).Nonempty) : IsBounded (pi univ S) ↔ ∀ i, IsBounded (S i)

Full source

theorem isBounded_pi_of_nonempty (hne : (pi univ S).Nonempty) :
    IsBoundedIsBounded (pi univ S) ↔ ∀ i, IsBounded (S i) :=
  ⟨fun H i => @eval_image_univ_pi _ _ _ i hne ▸ forall_isBounded_image_eval_iff.2 H i, IsBounded.pi⟩

Boundedness of Nonempty Product Sets via Componentwise Boundedness

Informal description

For a nonempty product set $\prod_{i \in I} S_i$ (where $I$ is the universal set of indices), the product set is bounded if and only if each component set $S_i$ is bounded.

Bornology.isBounded_pi theorem

: IsBounded (pi univ S) ↔ (∃ i, S i = ∅) ∨ ∀ i, IsBounded (S i)

Full source

theorem isBounded_pi : IsBoundedIsBounded (pi univ S) ↔ (∃ i, S i = ∅) ∨ ∀ i, IsBounded (S i) := by
  by_cases hne : ∃ i, S i = ∅
  · simp [hne, univ_pi_eq_empty_iff.2 hne]
  · simp only [hne, false_or]
    simp only [not_exists, ← Ne.eq_def, ← nonempty_iff_ne_empty, ← univ_pi_nonempty_iff] at hne
    exact isBounded_pi_of_nonempty hne

Boundedness Criterion for Product Sets: $\prod_{i} S_i$ is Bounded iff Some $S_i$ is Empty or All $S_i$ are Bounded

Informal description

For a family of sets $S_i \subseteq \pi_i$ indexed by $i \in \iota$, the product set $\prod_{i \in \iota} S_i$ is bounded if and only if either there exists an index $i$ such that $S_i$ is empty, or every set $S_i$ is bounded.

Bornology.isBounded_induced theorem

 {α β : Type*} [Bornology β] {f : α → β} {s : Set α} : @IsBounded α (Bornology.induced f) s ↔ IsBounded (f '' s)

Full source

theorem isBounded_induced {α β : Type*} [Bornology β] {f : α → β} {s : Set α} :
    @IsBounded α (Bornology.induced f) s ↔ IsBounded (f '' s) :=
  compl_mem_comap

Boundedness in Induced Bornology via Image

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a bornology, and let $f \colon \alpha \to \beta$ be a function. For any subset $s \subseteq \alpha$, $s$ is bounded in the bornology induced by $f$ if and only if the image $f(s)$ is bounded in $\beta$.

Bornology.isBounded_image_subtype_val theorem

{p : α → Prop} {s : Set { x // p x }} : IsBounded (Subtype.val '' s) ↔ IsBounded s

Full source

theorem isBounded_image_subtype_val {p : α → Prop} {s : Set { x // p x }} :
    IsBoundedIsBounded (Subtype.val '' s) ↔ IsBounded s :=
  isBounded_induced.symm

Boundedness of Subtype Image via Inclusion Map

Informal description

For any type $\alpha$ with a predicate $p$ and a subset $s$ of the subtype $\{x \mid p x\}$, the image of $s$ under the inclusion map $\text{Subtype.val}$ is bounded in $\alpha$ if and only if $s$ is bounded in the bornology of the subtype.

instBoundedSpaceProd instance

[BoundedSpace α] [BoundedSpace β] : BoundedSpace (α × β)

Full source

instance [BoundedSpace α] [BoundedSpace β] : BoundedSpace (α × β) := by
  simp [← cobounded_eq_bot_iff, cobounded_prod]

Boundedness of Product Spaces

Informal description

For any bounded spaces $\alpha$ and $\beta$, the product space $\alpha \times \beta$ is also a bounded space.

instBoundedSpaceForall instance

[∀ i, BoundedSpace (π i)] : BoundedSpace (∀ i, π i)

Full source

instance [∀ i, BoundedSpace (π i)] : BoundedSpace (∀ i, π i) := by
  simp [← cobounded_eq_bot_iff, cobounded_pi]

Boundedness of Product Spaces

Informal description

For any family of types $\pi_i$ indexed by $i$, if each $\pi_i$ is a bounded space, then the product type $\forall i, \pi_i$ is also a bounded space.

boundedSpace_induced_iff theorem

{α β : Type*} [Bornology β] {f : α → β} : @BoundedSpace α (Bornology.induced f) ↔ IsBounded (range f)

Full source

theorem boundedSpace_induced_iff {α β : Type*} [Bornology β] {f : α → β} :
    @BoundedSpace α (Bornology.induced f) ↔ IsBounded (range f) := by
  rw [← @isBounded_univ, isBounded_induced, image_univ]

Boundedness of Induced Bornology via Range of Function

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a bornology, and let $f \colon \alpha \to \beta$ be a function. The space $\alpha$ with the bornology induced by $f$ is a bounded space if and only if the range of $f$ is bounded in $\beta$.

boundedSpace_subtype_iff theorem

{p : α → Prop} : BoundedSpace (Subtype p) ↔ IsBounded {x | p x}

Full source

theorem boundedSpace_subtype_iff {p : α → Prop} :
    BoundedSpaceBoundedSpace (Subtype p) ↔ IsBounded { x | p x } := by
  rw [boundedSpace_induced_iff, Subtype.range_coe_subtype]

Boundedness of Subtype Space Equivalent to Boundedness of Predicate Set

Informal description

For any predicate $p$ on a type $\alpha$, the subtype $\{x \mid p x\}$ is a bounded space if and only if the set $\{x \mid p x\}$ is bounded in $\alpha$.

boundedSpace_val_set_iff theorem

{s : Set α} : BoundedSpace s ↔ IsBounded s

Full source

theorem boundedSpace_val_set_iff {s : Set α} : BoundedSpaceBoundedSpace s ↔ IsBounded s :=
  boundedSpace_subtype_iff

Boundedness of Subtype Equivalent to Boundedness of Set

Informal description

For any set $s$ in a type $\alpha$, the subtype $s$ is a bounded space if and only if the set $s$ is bounded in $\alpha$.

instBoundedSpaceSubtype instance

[BoundedSpace α] {p : α → Prop} : BoundedSpace (Subtype p)

Full source

instance [BoundedSpace α] {p : α → Prop} : BoundedSpace (Subtype p) :=
  (IsBounded.all { x | p x }).boundedSpace_subtype

Bounded Space Structure on Subtypes

Informal description

For any type $\alpha$ with a bounded space structure and any predicate $p$ on $\alpha$, the subtype $\{x \mid p x\}$ is also a bounded space.

instBornologyAdditive instance

: Bornology (Additive α)

Full source

instance : Bornology (Additive α) :=
  ‹Bornology α›

Bornology on Additive Groups

Informal description

The additive group of a type $\alpha$ inherits the bornology structure from $\alpha$.

instBornologyMultiplicative instance

: Bornology (Multiplicative α)

Full source

instance : Bornology (Multiplicative α) :=
  ‹Bornology α›

Bornology on Multiplicative Types

Informal description

The multiplicative version of a type $\alpha$ inherits the bornology structure from $\alpha$.

instBoundedSpaceAdditive instance

[BoundedSpace α] : BoundedSpace (Additive α)

Full source

instance [BoundedSpace α] : BoundedSpace (Additive α) :=
  ‹BoundedSpace α›

Bounded Space Structure on Additive Groups

Informal description

For any type $\alpha$ with a bounded space structure, the additive group of $\alpha$ also has a bounded space structure.

instBoundedSpaceMultiplicative instance

[BoundedSpace α] : BoundedSpace (Multiplicative α)

Full source

instance [BoundedSpace α] : BoundedSpace (Multiplicative α) :=
  ‹BoundedSpace α›

Bounded Space Structure on Multiplicative Types

Informal description

For any type $\alpha$ with a bounded space structure, the multiplicative version of $\alpha$ also has a bounded space structure.

instBornologyOrderDual instance

: Bornology αᵒᵈ

Full source

instance : Bornology αᵒᵈ :=
  ‹Bornology α›

Bornology Structure on Order Duals

Informal description

The order dual $\alpha^\text{op}$ of a type $\alpha$ inherits the bornology structure from $\alpha$.

instBoundedSpaceOrderDual instance

[BoundedSpace α] : BoundedSpace αᵒᵈ

Full source

instance [BoundedSpace α] : BoundedSpace αᵒᵈ :=
  ‹BoundedSpace α›

Bounded Space Structure on Order Duals

Informal description

For any type $\alpha$ with a bounded space structure, the order dual $\alpha^\text{op}$ also has a bounded space structure.