conditional_filter_eq_map_Ici — Mathlib

English

If γ is a Preorder with LocallyFiniteOrder and OrderTop, then (conditional γ).filter = atBot.map Finset.Ici.

Русский

Если γ — частичное упорядочение с локально конечным порядком и верхним элементом, то (conditional γ).filter = atBot.map Finset.Ici.

LaTeX

$$$(conditional \\gamma).\\mathrm{filter} = atBot.map Finset.Ici$$$

Lean4

/-- When `β` has a top element, `conditional β` is given by limits over finite intervals
`{y | x ≤ y}` as `x → atBot`. -/
@[simp high] -- want this to be prioritized over `conditional_filter` when they both apply

theorem conditional_filter_eq_map_Ici {γ} [PartialOrder γ] [LocallyFiniteOrder γ] [OrderTop γ] :
    (conditional γ).filter = atBot.map Finset.Ici := by simp [(isTop_top).atTop_eq, comp_def, Finset.Icc_top]

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