uIoc_injective_right — Mathlib

English

For fixed a, the map b ↦ Ι(b,a) is injective.

Русский

Для фиксированного a отображение b ↦ Ι(b,a) инъективно.

LaTeX

$$$ \\text{Injective}(\\lambda b. Ι(b,a)) $$$

Lean4

theorem uIoc_injective_right (a : α) : Injective fun b => Ι b a :=
  by
  rintro b c h
  rw [Set.ext_iff] at h
  obtain ha | ha := le_or_gt b a
  · have hb := (h b).not
    simp only [ha, left_mem_uIoc, true_iff, notMem_uIoc, ← not_le, and_true, not_true, false_and, not_false_iff,
      or_false] at hb
    refine hb.eq_of_not_lt fun hc => ?_
    simpa [ha, and_iff_right hc, ← @not_le _ _ _ a, iff_not_self, -not_le] using h c
  · refine eq_of_mem_uIoc_of_mem_uIoc ((h _).1 <| left_mem_uIoc.2 ha) ((h _).2 <| left_mem_uIoc.2 <| ha.trans_le ?_)
    simpa [ha, ha.not_ge, mem_uIoc] using h b

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