Ioc_inl_inl — Mathlib

English

In Lex, the half-open interval from a left-embedded to a left-embedded element equals the image of the corresponding interval in α under the embedding into the Lex sum.

Русский

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

LaTeX

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

Lean4

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

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