wcovBy_iff_le_and_eq_or_eq — Mathlib

English

An equivalence: a ⩿ b iff a ≤ b and every c with a ≤ c ≤ b is equal to a or b.

Русский

Эквивалентность: a ⩿ b тогда и только тогда, когда a ≤ b и для любого c с a ≤ c ≤ b выполняется c = a или c = b.

LaTeX

$$$$a\,⩿\, b \iff (a\le b) \land \forall c, a\le c \to c \le b \to (c=a) \lor (c=b).$$$$

Lean4

/-- An `iff` version of `WCovBy.eq_or_eq` and `wcovBy_of_eq_or_eq`. -/
theorem wcovBy_iff_le_and_eq_or_eq : a ⩿ b ↔ a ≤ b ∧ ∀ c, a ≤ c → c ≤ b → c = a ∨ c = b :=
  ⟨fun h => ⟨h.le, fun _ => h.eq_or_eq⟩, And.rec wcovBy_of_eq_or_eq⟩

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