Ioo_inl_inl — Mathlib

English

In Lex, the open interval between two left-embedded elements is the image of the corresponding open interval in α via the embedding into the Lex sum.

Русский

В Lex открытый интервал между двумя левыми встроенными элементами является образом соответствующего открытого интервала в α через встроение в Lex.

LaTeX

$$$ \operatorname{Ioo}(\mathrm{inl}_\ell a_1)(\mathrm{inl}_\ell a_2) = \operatorname{map}(\mathrm{Embedding.inl} \circ toLex.toEmbedding)(\operatorname{Ioo} a_1 a_2) $$$

Lean4

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

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