Mathlib Map

Theorems · Theorem · order theory

infClosed_pi

∀ {ι : Type u_6} {α : ι → Type u_7} [inst : (i : ι) → SemilatticeInf (α i)] {s : Set ι} {t : (i : ι) → Set (α i)},
  (∀ i ∈ s, InfClosed (t i)) → InfClosed (s.pi t)
Defined in
Mathlib.Order.SupClosed
Cited by
1 results in Mathlib
Foundations
Depth 15 from the axioms · uses Quot.sound
Assumes
SemilatticeInf
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

isSublattice_pi · cited by 0isSublattice_piSet · cited by 53352SetSemilatticeInf · cited by 634SemilatticeInfSet.pi · cited by 405Set.piInfClosed · cited by 57InfClosedinfClosed_piCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement and proof · cited by 53,352
  • SemilatticeInfstatement and proof · cited by 634
  • Set.pistatement and proof · cited by 405
  • InfClosedstatement and proof · cited by 57

Cited by1

Results whose statement or proof uses this declaration.