exists_ne_zero_and_le_and_le — Mathlib

English

Given x ≠ 0 and y ≠ 0 in WithZero α, there exists z in WithZero α with z ≠ 0 and z ≤ x and z ≤ y.

Русский

Пусть x ≠ 0 и y ≠ 0 в WithZero α. Существует z ∈ WithZero α such that z ≠ 0 и z ≤ x и z ≤ y.

LaTeX

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

Lean4

theorem exists_ne_zero_and_le_and_le (hx : x ≠ 0) (hy : y ≠ 0) : ∃ z, z ≠ 0 ∧ z ≤ x ∧ z ≤ y :=
  ⟨x ⊓ y, by simp [min_eq_iff, hx, hy], by simp, by simp⟩

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