eq_of_ge_of_le — Mathlib

English

If f is antitone and f(a) = f(b), then for every i with a ≤ i ≤ b, f(i) = f(a).

Русский

Если f антитонична и f(a) = f(b), то для i между a и b выполняется f(i) = f(a).

LaTeX

$$$ (hf : Antitone f) \rightarrow f a = f b \rightarrow \forall i, a \le i \rightarrow i \le b \rightarrow f i = f a $$$

Lean4

/-- If an antitone function is equal at two points, it is equal between all of them -/
theorem eq_of_ge_of_le {a₁ a₂ : α} (h_anti : Antitone f) (h_fa : f a₁ = f a₂) {i : α} (h₁ : a₁ ≤ i) (h₂ : i ≤ a₂) :
    f i = f a₁ := by
  apply le_antisymm
  · exact h_anti h₁
  · rw [h_fa]; exact h_anti h₂

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