isReflection_of_mem_leftInvSeq — Mathlib

English

If t belongs to the left-inverse sequence lis ω, then t is a reflection.

Русский

Если t принадлежит левой инверсной последовательности lis ω, то t — отражение.

LaTeX

$$$t \\in \\mathrm{lis}(\\omega) \\Rightarrow cs.IsReflection(t)$$$

Lean4

theorem isReflection_of_mem_leftInvSeq (ω : List B) {t : W} (ht : t ∈ lis ω) : cs.IsReflection t :=
  by
  simp only [leftInvSeq_eq_reverse_rightInvSeq_reverse, mem_reverse] at ht
  exact cs.isReflection_of_mem_rightInvSeq ω.reverse ht

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