mem_range_embedding_iff' — Mathlib

English

For any j ∈ Fin n and i ∈ Fin c.length, j lies in the range of embedding i if and only if i equals index j: j ∈ Set.range (c.embedding i) ⇔ i = c.index j.

Русский

Для любой пары j ∈ Fin n и i ∈ Fin c.length верно: j принадлежит диапазону вложения i тогда, когда i равен индексу j: j ∈ range (c.embedding i) ⇔ i = c.index j.

LaTeX

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

Lean4

theorem mem_range_embedding_iff' {j : Fin n} {i : Fin c.length} : j ∈ Set.range (c.embedding i) ↔ i = c.index j :=
  by
  constructor
  · rw [← not_imp_not]
    intro h
    exact Set.disjoint_right.1 (c.disjoint_range h) (c.mem_range_embedding j)
  · intro h
    rw [h]
    exact c.mem_range_embedding j

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