Ioc_inr_inl — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem Ioc_inr_inl : Ioc (inrₗ b) (inlₗ a) = ∅ :=
  rfl

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