monotone_defaultRatCDF

Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.monotone_defaultRatCDF

← MathLib Explorer

English

The function defaultRatCDF is monotone increasing.

Русский

Функция defaultRatCDF монотонно возрастает.

LaTeX

$$$\\mathrm{Monotone}(\\mathrm{defaultRatCDF})$$$

Lean4

theorem monotone_defaultRatCDF : Monotone defaultRatCDF :=
  by
  unfold defaultRatCDF
  intro x y hxy
  dsimp only
  split_ifs with h_1 h_2 h_2
  exacts [le_rfl, zero_le_one, absurd (hxy.trans_lt h_2) h_1, le_rfl]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru