exists_square_le — Mathlib

English

For every a in α with MulLeftStrictMono, there exists b with b^2 ≤ a.

Русский

Для каждого a в α с MulLeftStrictMono существует b, такой что b^2 ≤ a.

LaTeX

$$$\\\\forall a \\\\in \\\\alpha, \\\\exists b \\\\in \\\\alpha, b \\\\cdot b \\\\le a$$$

Lean4

theorem exists_square_le [MulLeftStrictMono α] (a : α) : ∃ b : α, b * b ≤ a :=
  by
  by_cases h : a < 1
  · use a
    have : a * a < a * 1 := mul_lt_mul_left' h a
    rw [mul_one] at this
    exact le_of_lt this
  · use 1
    push_neg at h
    rwa [mul_one]

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