Theorems · Theorem · order theory

Sublattice.le_pi

∀ {κ : Type u_5} {π : κ → Type u_6} [inst : (i : κ) → Lattice (π i)] {s : Set κ} {L : (i : κ) → Sublattice (π i)}
  {M : Sublattice ((i : κ) → π i)}, M ≤ Sublattice.pi s L ↔ ∀ i ∈ s, M ≤ Sublattice.comap (Pi.evalLatticeHom i) (L i)

Defined in

Mathlib.Order.Sublattice

Cited by

0 results in Mathlib

Foundations

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

Assumes

Lattice