Iic_inl — Mathlib

English

In Lex, the closed down-set below a left-embedded a equals the image under inl of the closed down-set below a in α, composed with toLex.

Русский

В Lex замкнутое множество ниже левого встроенного a эквивалентно изображению через inl замкнутого множества ниже a в α, затем через toLex.

LaTeX

$$$ \operatorname{Iic}(\mathrm{inl}_\ell a) = \mathrm{map}(\mathrm{Embedding.inl} .\mathrm{trans} toLex.toEmbedding)(\operatorname{Iic} a) $$$

Lean4

theorem Iic_inl : Iic (inlₗ a : α ⊕ₗ β) = (Iic a).map (Embedding.inl.trans toLex.toEmbedding) :=
  rfl

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