lt_inducedMap_iff — Mathlib

English

Let a ∈ α and b ∈ β. Then b < inducedMap α β a holds iff there exists a rational q with b < q and (q : α) < a.

Русский

Пусть a ∈ α и b ∈ β. Тогда b < inducedMap α β a эквивалентно существованию рационального q с b < q и (q : α) < a.

LaTeX

$$$ b < \\operatorname{inducedMap}_{\\alpha,\\beta} a \\iff \\exists q \\in \\mathbb{Q},\\; b < q \\land (q : \\alpha) < a $$$

Lean4

theorem lt_inducedMap_iff : b < inducedMap α β a ↔ ∃ q : ℚ, b < q ∧ (q : α) < a :=
  ⟨fun h => (exists_rat_btwn h).imp fun _ => And.imp_right coe_lt_inducedMap_iff.1, fun ⟨q, hbq, hqa⟩ =>
    hbq.trans <| by rwa [coe_lt_inducedMap_iff]⟩

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