isSublattice_pi — Mathlib

English

If for every i in a set s the set t(i) is a Sublattice, then the Pi-type set s.pi t is a Sublattice.

Русский

Если для каждого i в s множество t(i) является субрешеткой, тогда множество пи-типа s.pi t является субрешеткой.

LaTeX

$$ (∀ i, i ∈ s → IsSublattice (t i)) → IsSublattice (s.pi t)$$

Lean4

theorem isSublattice_pi {ι : Type*} {α : ι → Type*} [∀ i, Lattice (α i)] {s : Set ι} {t : ∀ i, Set (α i)}
    (ht : ∀ i ∈ s, IsSublattice (t i)) : IsSublattice (s.pi t) :=
  ⟨supClosed_pi fun _i hi ↦ (ht _ hi).1, infClosed_pi fun _i hi ↦ (ht _ hi).2⟩

Похожие утверждения