image_coe_Ioc — Mathlib

English

The image of Ioc(a,b) under i is Ioc(i(a), i(b)).

Русский

Образ Ioc(a,b) под i равен Ioc(i(a), i(b)).

LaTeX

$$$$ i''(\mathrm{Ioc}(a,b)) = \mathrm{Ioc}(\mathrm{i}(a), \mathrm{i}(b)) $$$$

Lean4

theorem image_coe_Ioc : (some : α → WithTop α) '' Ioc a b = Ioc (a : WithTop α) b := by
  rw [← preimage_coe_Ioc, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Subset.trans Ioc_subset_Iic_self <| Iic_subset_Iio.2 <| coe_lt_top b)]

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