forall_le_coe_iff_le — Mathlib

English

For x,y ∈ WithBot α under NoBotOrder α, the condition (∀ a : α, y ≤ a → x ≤ a) is equivalent to x ≤ y.

Русский

Для x, y ∈ WithBot α при NoBotOrder α условие (∀ a ∈ α, y ≤ a → x ≤ a) эквивалентно x ≤ y.

LaTeX

$$$ (\forall a : \alpha, y ≤ a \rightarrow x \le a) \iff x \le y $$$

Lean4

theorem forall_le_coe_iff_le [NoBotOrder α] : (∀ a : α, y ≤ a → x ≤ a) ↔ x ≤ y :=
  by
  obtain _ | y := y
  · simp [WithBot.none_eq_bot, eq_bot_iff_forall_le]
  · exact ⟨fun h ↦ h _ le_rfl, fun hmn a ham ↦ hmn.trans ham⟩

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