mem_range_embedding — Mathlib

English

For any c and j, the element j lies in the range of the embedding of its containing block: j ∈ Set.range (c.embedding (c.index j)).

Русский

Пусть c — композиция, и j — индекс элемента; тогда j принадлежит диапазону вложения блока, содержащего этот элемент: j ∈ range (c.embedding (c.index j)).

LaTeX

$$$ j \\in \\mathrm{Set.range}(c.embedding (c.index j)) $$$

Lean4

theorem mem_range_embedding (j : Fin n) : j ∈ Set.range (c.embedding (c.index j)) :=
  by
  have : c.embedding (c.index j) (c.invEmbedding j) ∈ Set.range (c.embedding (c.index j)) := Set.mem_range_self _
  rwa [c.embedding_comp_inv j] at this

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