Theorems · Theorem · general topology

Antitone.piecewise_eventually_eq_iInter

∀ {ι : Type u_1} {α : Type u_3} {β : α → Type u_6} [inst : Preorder ι] {s : ι → Set α}
  [inst_1 : (i : ι) → DecidablePred fun x => x ∈ s i] [inst_2 : DecidablePred fun x => x ∈ ⋂ i, s i],
  Antitone s →
    ∀ (f g : (a : α) → β a) (a : α), ∀ᶠ (i : ι) in Filter.atTop, (s i).piecewise f g a = (⋂ i, s i).piecewise f g a

Defined in

Mathlib.Order.Filter.AtTopBot.Defs

Cited by

2 results in Mathlib

Foundations

Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PreorderDecidablePredDecidablePred