Theorems · Theorem · order theory
Sublattice.coe_pi
∀ {κ : Type u_5} {π : κ → Type u_6} [inst : (i : κ) → Lattice (π i)] (s : Set κ) (L : (i : κ) → Sublattice (π i)),
↑(Sublattice.pi s L) = s.pi fun i => ↑(L i)- Defined in
- Mathlib.Order.Sublattice
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses Quot.sound
- Assumes
- Lattice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- SetLike.coestatement and proof · cited by 8,199
- Latticestatement and proof · cited by 916
- Set.pistatement · cited by 405
- Sublatticestatement and proof · cited by 225
- Sublattice.pistatement and proof · cited by 9
Cited by1
Results whose statement or proof uses this declaration.
- Sublattice.pi_univ_eq_bot_iffproof · cited by 1