isSublattice_iInter — Mathlib

English

If each f i is a Sublattice, then the infinite intersection ⋂ i, f i is a Sublattice.

Русский

Если каждый f i является субрешеткой, то бесконечная пересечение ⋂ i, f i — субрешетка.

LaTeX

$$ (∀ i, IsSublattice (f i)) → IsSublattice (Set.iInter (fun i => f i))$$

Lean4

theorem isSublattice_iInter (hf : ∀ i, IsSublattice (f i)) : IsSublattice (⋂ i, f i) :=
  ⟨supClosed_iInter fun _i ↦ (hf _).1, infClosed_iInter fun _i ↦ (hf _).2⟩

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