eq_of_forall_le_coe_iff — Mathlib

English

If h says that for every a ∈ α, x ≤ a is equivalent to y ≤ a, then x = y.

Русский

Если дано, что для каждого a ∈ α выполняется x ≤ a ⇔ y ≤ a, тогда x = y.

LaTeX

$$$ (\forall a : \alpha, x ≤ a \leftrightarrow y ≤ a) \Rightarrow x = y $$$

Lean4

theorem eq_of_forall_le_coe_iff (h : ∀ a : α, x ≤ a ↔ y ≤ a) : x = y :=
  le_antisymm (forall_le_coe_iff_le.mp fun a ↦ (h a).2) (forall_le_coe_iff_le.mp fun a ↦ (h a).1)

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