exists_ne_zero_and_lt_and_lt — Mathlib

English

Given x ≠ 0 and y ≠ 0 in WithZero α, there exists z ≠ 0 with z < x and z < y provided NoMinOrder on α.

Русский

Пусть x ≠ 0 и y ≠ 0 в WithZero α; существует z ≠ 0 such that z < x и z < y, при условии NoMinOrder на α.

LaTeX

$$$\exists z:\mathrm{WithZero}\,\alpha,\ z \neq 0 \land z < x \land z < y$$$

Lean4

theorem exists_ne_zero_and_lt_and_lt [NoMinOrder α] (hx : x ≠ 0) (hy : y ≠ 0) : ∃ z, z ≠ 0 ∧ z < x ∧ z < y :=
  by
  obtain ⟨z', hnz', hzx, hzy⟩ := exists_ne_zero_and_le_and_le hx hy
  obtain ⟨z, hnz, hlt⟩ := exists_ne_zero_and_lt hnz'
  use z, hnz
  constructor <;> exact lt_of_lt_of_le hlt ‹z' ≤ _›

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