Theorems · Theorem · order theory

OrderIso.liminf_apply

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_6} [inst : ConditionallyCompleteLattice β]
  [inst_1 : ConditionallyCompleteLattice γ] {f : Filter α} {u : α → β} (g : β ≃o γ),
  autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) OrderIso.liminf_apply._auto_1 →
    autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f u) OrderIso.liminf_apply._auto_3 →
      autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f fun x => g (u x)) OrderIso.liminf_apply._auto_5 →
        autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f fun x => g (u x)) OrderIso.liminf_apply._auto_7 →
          g (Filter.liminf u f) = Filter.liminf (fun x => g (u x)) f

Defined in

Mathlib.Order.LiminfLimsup

Cited by

6 results in Mathlib

Foundations

Depth 29 from the axioms · uses propext, Quot.sound

Assumes

ConditionallyCompleteLatticeConditionallyCompleteLattice