conditional_filter_eq_map_Iic — Mathlib

English

If γ is a PartialOrder with LocallyFiniteOrder and has a bottom element, then (conditional γ).filter = atTop.map Finset.Iic.

Русский

Если γ частично упорядочено, локально конечна, и есть нижний элемент, то (conditional γ).filter = atTop.map Finset.Iic.

LaTeX

$$$(conditional \\gamma).\\mathrm{filter} = atTop.map Finset.Iic$$$

Lean4

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

theorem conditional_filter_eq_map_Iic {γ} [PartialOrder γ] [LocallyFiniteOrder γ] [OrderBot γ] :
    (conditional γ).filter = atTop.map Finset.Iic := by simp [(isBot_bot).atBot_eq, comp_def, Finset.Icc_bot]

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