Documentation

MeanFourier.Mathlib.Topology.Bornology.Basic

Bounded functions #

source
def Bornology.IsBddFun {α : Type u_1} {X : Type u_2} [Bornology X] (f : α → X) :
Prop
Equations
Instances For
    source
    @[simp]
    theorem Bornology.IsBddFun.const {α : Type u_1} {X : Type u_2} [Bornology X] {x : X} :
    IsBddFun (Function.const α x)
    source
    @[simp]
    theorem Bornology.IsBddFun.fun_const {α : Type u_1} {X : Type u_2} [Bornology X] {x : X} :
    IsBddFun fun (x_1 : α) => x

    Eta-expanded form of Bornology.IsBddFun.const

    source
    @[simp]
    theorem Bornology.IsBddFun.one {α : Type u_1} {X : Type u_2} [Bornology X] [One X] :
    IsBddFun 1
    source
    @[simp]
    theorem Bornology.IsBddFun.zero {α : Type u_1} {X : Type u_2} [Bornology X] [Zero X] :
    IsBddFun 0
    source
    @[simp]
    theorem Bornology.IsBddFun.natCast {α : Type u_1} {X : Type u_2} [Bornology X] [NatCast X] {n : ℕ} :
    IsBddFun ↑n
    source
    @[simp]
    theorem Bornology.IsBddFun.ofNat {α : Type u_1} {X : Type u_2} [Bornology X] [NatCast X] {n : ℕ} [n.AtLeastTwo] :
    IsBddFun (OfNat.ofNat n)
    source
    @[simp]
    theorem Bornology.IsBddFun.intCast {α : Type u_1} {X : Type u_2} [Bornology X] [IntCast X] {n : ℤ} :
    IsBddFun ↑n
    source
    theorem Bornology.IsBddFun.of_finite {α : Type u_1} {X : Type u_2} [Bornology X] {f : α → X} [Finite α] :
    IsBddFun f