not_wcovBy_iff — Mathlib

English

If a ≤ b, then a does not cover b iff there exists an element strictly between a and b.

Русский

Если a ≤ b, то a не покрывает b тогда и только тогда, когда существует элемент строго между a и b.

LaTeX

$$$a \\\\le b \\\\Rightarrow (\\\\neg (a \\\\mathrel{\\\\trianglelefteq} b) \\\\iff \\\\exists c, a < c \\\\land c < b).$$$

Lean4

/-- If `a ≤ b`, then `b` does not cover `a` iff there's an element in between. -/
theorem not_wcovBy_iff (h : a ≤ b) : ¬a ⩿ b ↔ ∃ c, a < c ∧ c < b := by
  simp_rw [WCovBy, h, true_and, not_forall, exists_prop, not_not]

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