LocallyBoundedMapClass.comap_cobounded_le
theorem LocallyBoundedMapClass.comap_cobounded_le :
∀ {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} [inst : Bornology α] [inst_1 : Bornology β]
[inst_2 : FunLike F α β] [self : LocallyBoundedMapClass F α β] (f : F),
Filter.comap (⇑f) (Bornology.cobounded β) ≤ Bornology.cobounded α
The theorem `LocallyBoundedMapClass.comap_cobounded_le` states that, for all types `F`, `α`, and `β` whereby `α` and `β` have a Bornology (a structure defining a collection of bounded sets in a topology), and there exists an injective function `f` of type `F` that maps `α` to `β`, then the pullback of the `Bornology.cobounded` filter (a filter of sets that are not bounded) under `f` is contained in the `Bornology.cobounded` filter of `α`. In other words, the function `f` maps bounded sets to bounded sets.
More concisely: If `F` is a type, `α` and `β` have Bornologies, and there exists an injective function `f : α → β` between them, then the pullback of the cobounded filter of `β` under `f` is contained in the cobounded filter of `α`.
|
LocallyBoundedMap.ext
theorem LocallyBoundedMap.ext :
∀ {α : Type u_2} {β : Type u_3} [inst : Bornology α] [inst_1 : Bornology β] {f g : LocallyBoundedMap α β},
(∀ (a : α), f a = g a) → f = g
This theorem states that for any two locally bounded maps `f` and `g` from a type `α` with a bornology to a type `β` also with a bornology, if the maps `f` and `g` are equal for all elements of type `α`, then `f` and `g` themselves are equal. In mathematical terms, if two locally bounded maps have the same effect on all elements of their domain, they are, in fact, the same map.
More concisely: If two locally bounded maps from a bornology-equipped type to another bornology-equipped type agree on all elements, they are equal.
|
LocallyBoundedMap.comap_cobounded_le'
theorem LocallyBoundedMap.comap_cobounded_le' :
∀ {α : Type u_6} {β : Type u_7} [inst : Bornology α] [inst_1 : Bornology β] (self : LocallyBoundedMap α β),
Filter.comap self.toFun (Bornology.cobounded β) ≤ Bornology.cobounded α
The theorem, named `LocallyBoundedMap.comap_cobounded_le'`, states that for any two types `α` and `β`, both equipped with a bornology (a type of structure that describes boundedness in a topological space), and a locally bounded map from `α` to `β`, the preimage of the filter of cobounded sets in `β` under this map is contained within the filter of cobounded sets in `α`. In other words, this map sends bounded sets in `α` to bounded sets in `β`. The term "cobounded sets" refers to sets that are not exceeded in size by any bounded set.
More concisely: Given types `α` and `β` with bornologies, and a locally bounded map from `α` to `β`, the preimage of the filter of cobounded sets in `β` under this map is included in the filter of cobounded sets in `α`.
|