Bornology.IsBounded.boundedSpace_subtype
theorem Bornology.IsBounded.boundedSpace_subtype :
∀ {α : Type u_1} [inst : Bornology α] {p : α → Prop}, Bornology.IsBounded {x | p x} → BoundedSpace (Subtype p) := by
sorry
The theorem `Bornology.IsBounded.boundedSpace_subtype` is a alias of the reverse direction of the theorem `boundedSpace_subtype_iff`. It states that for any type `α` with a bornology structure and any predicate `p` on `α`, if the set of elements `{x | p x}` in `α` that satisfy the predicate `p` is bounded relative to the ambient bornology on `α`, then the subtype `Subtype p` of `α` determined by `p` is a bounded space. In other words, it establishes a connection between the boundedness of a set in the context of bornology and the boundedness of a subtype.
More concisely: If a subtype of a bornology space, determined by a predicate, is bounded in the given bornology, then the subtype itself is a bounded space.
|
Bornology.forall_isBounded_image_eval_iff
theorem Bornology.forall_isBounded_image_eval_iff :
∀ {ι : Type u_3} {π : ι → Type u_4} [inst : (i : ι) → Bornology (π i)] {s : Set ((i : ι) → π i)},
(∀ (i : ι), Bornology.IsBounded (Function.eval i '' s)) ↔ Bornology.IsBounded s
This theorem states that for any type `ι`, any function `π` from `ι` to some type, and for every set `s` of functions from `ι` to `π i` (where we have a bornology on each `π i`), the set `s` is bounded if and only if the image of each function `Function.eval i` (which takes each function in `s` and applies it to `i`) is bounded with regard to the bornology on `π i`. In simpler terms, it tells us that a set of functions is bounded if and only if, when we apply each function to each possible input, we always get a bounded set.
More concisely: For any type `ι`, a set `s` of functions from `ι` to some type `π` is bounded (with respect to the bornology on each `π i`) if and only if the image under `Function.eval` of every function in `s` is a bounded set (with respect to the bornology on `π i`).
|
Bornology.IsBounded.boundedSpace_val
theorem Bornology.IsBounded.boundedSpace_val :
∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, Bornology.IsBounded s → BoundedSpace ↑s
The theorem `Bornology.IsBounded.boundedSpace_val` states that for any type `α` equipped with a bornology, and any set `s` of `α`, if `s` is bounded relative to the ambient bornology on `α` (denoted by `Bornology.IsBounded s`), then the set `s` can be thought of as a bounded space (denoted by `BoundedSpace ↑s`). In other words, this theorem provides a condition under which we can view a set as a bounded space within the context of a bornology.
More concisely: If a set in a bornology-equipped type is bounded, then it can be considered a bounded space within that bornology.
|
Bornology.isBounded_image_fst_and_snd
theorem Bornology.isBounded_image_fst_and_snd :
∀ {α : Type u_1} {β : Type u_2} [inst : Bornology α] [inst_1 : Bornology β] {s : Set (α × β)},
Bornology.IsBounded (Prod.fst '' s) ∧ Bornology.IsBounded (Prod.snd '' s) ↔ Bornology.IsBounded s
The theorem `Bornology.isBounded_image_fst_and_snd` states that for any sets `s` of pairs from two types `α` and `β` with bornologies, the set `s` is bounded if and only if the images of `s` under the first (`Prod.fst`) and second (`Prod.snd`) projection functions are both bounded. In other words, `s` is bounded in the product bornology precisely when its projections onto each factor are bounded in their respective bornologies.
More concisely: A set of pairs in the product of two types with bornologies is bounded if and only if the images of the set under the first and second projection functions are both boundedly covered.
|