coe_lt_inducedMap_iff — Mathlib

English

For every a and every rational q, the order relation between q and a is preserved under the induced map: (q in β) < inducedMap α β a iff (q in α) < a.

Русский

Для любых a и рационального q порядок между q и a сохраняется под индуцированным отображением: (q в β) < inducedMap α β a эквивалентно (q в α) < a.

LaTeX

$$$ (q : \\beta) < \\operatorname{inducedMap} \\alpha \\beta a \\;\\iff\\; (q : \\alpha) < a $$$

Lean4

theorem coe_lt_inducedMap_iff : (q : β) < inducedMap α β a ↔ (q : α) < a :=
  by
  refine ⟨fun h => ?_, fun hq => ?_⟩
  · rw [← inducedMap_rat α] at h
    exact (inducedMap_mono α β).reflect_lt h
  · obtain ⟨q', hq, hqa⟩ := exists_rat_btwn hq
    apply lt_csSup_of_lt (cutMap_bddAbove β a) (coe_mem_cutMap_iff.mpr hqa)
    exact mod_cast hq

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