chainHeight_eq_iSup_Iic — Mathlib

English

The chainHeight equals the supremum over i in s of the chainHeight of the intersection with Iic(i).

Русский

Цепная высота равна верхней гранью по i ∈ s от chainHeight( s ∩ Iic(i) ).

LaTeX

$$s.chainHeight = ⨆ i ∈ s, (s ∩ Set.Iic i).chainHeight$$

Lean4

theorem chainHeight_eq_iSup_Iic : s.chainHeight = ⨆ i ∈ s, (s ∩ Set.Iic i).chainHeight :=
  by
  simp_rw [← chainHeight_dual (_ ∩ _)]
  rw [← chainHeight_dual, chainHeight_eq_iSup_Ici]
  rfl

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