pow_two_semiclosed — Mathlib

English

In a lattice-ordered group, if 1 ≤ a^2 then 1 ≤ a.

Русский

В группе с решёткой: если 1 ≤ a^2, то 1 ≤ a.

LaTeX

$$$ 1 \le a^{2} \;\Rightarrow\; 1 \le a $$$

Lean4

@[to_additive]
theorem pow_two_semiclosed {a : α} (ha : 1 ≤ a ^ 2) : 1 ≤ a :=
  by
  suffices this : (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1 by rwa [← inf_eq_right, ← mul_eq_left]
  rw [mul_inf, inf_mul, ← pow_two, mul_one, one_mul, inf_assoc, inf_left_idem, inf_comm, inf_assoc, inf_of_le_left ha]

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