inducedMap_rat — Mathlib

English

For any rational q, inducedMap α β (q : α) equals q viewed in β.

Русский

Для рационального q отображение inducedMap α β (q : α) равно q, как элемент β.

LaTeX

$$$\\mathrm{inducedMap}(q : α) = q : β$$$

Lean4

theorem inducedMap_rat (q : ℚ) : inducedMap α β (q : α) = q :=
  by
  refine csSup_eq_of_forall_le_of_forall_lt_exists_gt (cutMap_nonempty β (q : α)) (fun x h => ?_) fun w h => ?_
  · rw [cutMap_coe] at h
    obtain ⟨r, h, rfl⟩ := h
    exact le_of_lt h
  · obtain ⟨q', hwq, hq⟩ := exists_rat_btwn h
    rw [cutMap_coe]
    exact ⟨q', ⟨_, hq, rfl⟩, hwq⟩

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