mul_lt_of_lt — Mathlib

English

If c is at least countable and a < c and b < c, then a · b < c.

Русский

Пусть c не меньше ℵ₀, и a, b кардиналы с a < c и b < c. Тогда произведение a и b строго меньше c.

LaTeX

$$$$(\aleph_0 \le c) \land (a < c) \land (b < c) \Rightarrow a \cdot b < c$$$$

Lean4

theorem mul_lt_of_lt {a b c : Cardinal} (hc : ℵ₀ ≤ c) (h1 : a < c) (h2 : b < c) : a * b < c :=
  (mul_le_mul' (le_max_left a b) (le_max_right a b)).trans_lt <|
    (lt_or_ge (max a b) ℵ₀).elim (fun h => (mul_lt_aleph0 h h).trans_le hc) fun h =>
      by
      rw [mul_eq_self h]
      exact max_lt h1 h2

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