Ioo_inr_inr — Mathlib

English

In Lex, the open interval between two right-embedded elements maps to the image of (Ioi b1) disjSum (Iio b2) under toLex embeddings.

Русский

В Lex открытый интервал между двумя правыми встроенными элементами отображается как образ (Ioi b1) disjSum (Iio b2) через toLex.

LaTeX

$$$ \operatorname{Ioo}(\mathrm{inr}_\ell b_1)(\mathrm{inr}_\ell b_2) = ((\mathrm{Ioi} b_1).\mathrm{disjSum}(\mathrm{Iio} b_2)).\mathrm{map} toLex.toEmbedding $$$

Lean4

theorem Ioo_inr_inr : Ioo (inrₗ b₁ : α ⊕ₗ β) (inrₗ b₂) = (Ioo b₁ b₂).map (Embedding.inr.trans toLex.toEmbedding) := by
  rw [← Finset.map_map]; rfl

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