chainHeight_le_chainHeight_iff — Mathlib

English

The inequality s.chainHeight ≤ t.chainHeight is equivalent to the existence of matching subchains with equal lengths for all chains in s.subchain.

Русский

Неравенство chainHeight между s и t эквивалентно существованию соответствующих подцепочек с равными длинами для всех цепочек в s.subchain.

LaTeX

$$s.chainHeight ≤ t.chainHeight ↔ ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, length l = length l'$$

Lean4

theorem chainHeight_le_chainHeight_iff {t : Set β} :
    s.chainHeight ≤ t.chainHeight ↔ ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, length l = length l' :=
  (chainHeight_le_chainHeight_TFAE s t).out 0 1

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