Iic_toDual — Mathlib

English

In the dual order, the statement Iic(toDual a) equals (Ici (ofDual a)).map toDual.toEmbedding expresses the same fact as in the dual setting.

Русский

В двойственном порядке равенство Iic(toDual a) = (Ici (ofDual a)).map toDual.toEmbedding выражает то же свойство в двойственной обстановке.

LaTeX

$$$ Iic (toDual a) = (Ici (ofDual a)).map toDual.toEmbedding $$$

Lean4

theorem Iic_toDual (a : α) : Iic (toDual a) = (Ici a).map toDual.toEmbedding :=
  map_refl.symm

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