isRatStieltjesPoint_unit_prod_iff

English

IsRatStieltjesPoint for a function f on α extended by Unit equals IsRatStieltjesPoint of f on α.

Русский

IsRatStieltjesPoint при добавлении единичного компонента равенство с исходной функцией.

LaTeX

$$$IsRatStieltjesPoint\\left( (p : Unit × α) \\mapsto f(p.2) \\right) ((),a) \\iff IsRatStieltjesPoint f a$$$

Lean4

theorem isRatStieltjesPoint_unit_prod_iff (f : α → ℚ → ℝ) (a : α) :
    IsRatStieltjesPoint (fun p : Unit × α ↦ f p.2) ((), a) ↔ IsRatStieltjesPoint f a := by
  constructor <;> exact fun h ↦ ⟨h.mono, h.tendsto_atTop_one, h.tendsto_atBot_zero, h.iInf_rat_gt_eq⟩

Похожие утверждения