chainHeight_le_chainHeight_iff_le

English

The inequality s.chainHeight ≤ t.chainHeight is equivalent to the existence, for every chain l in s.subchain, of a chain l' in t.subchain with length l not exceeding length l'.

Русский

Неравенство chainHeight между s и t эквивалентно существованию для каждой цепи l ∈ s.subchain цепи l' ∈ t.subchain с длиной l ≤ длина l'.

LaTeX

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

Lean4

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

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