veblenWith_le_veblenWith_iff_right

English

For normal f, veblenWith f o a ≤ veblenWith f o b if and only if a ≤ b.

Русский

Для нормальной f верна эквивалентность: veblenWith f o a ≤ veblenWith f o b ⇔ a ≤ b.

LaTeX

$$theorem veblenWith_le_veblenWith_iff_right : veblenWith f o a ≤ veblenWith f o b ↔ a ≤ b$$

Lean4

@[simp]
theorem veblenWith_le_veblenWith_iff_right : veblenWith f o a ≤ veblenWith f o b ↔ a ≤ b :=
  (veblenWith_right_strictMono hf o).le_iff_le

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