isSublattice_sInter — Mathlib

English

If every member s ∈ S is a Sublattice, then the intersection ⋂ S is a Sublattice.

Русский

Если каждый элемент множества S является субрешеткой, то общая пересечение ⋂ S является субрешеткой.

LaTeX

$$ (∀ s ∈ S, IsSublattice s) → IsSublattice (⋂₀ S)$$

Lean4

theorem isSublattice_sInter (hS : ∀ s ∈ S, IsSublattice s) : IsSublattice (⋂₀ S) :=
  ⟨supClosed_sInter fun _s hs ↦ (hS _ hs).1, infClosed_sInter fun _s hs ↦ (hS _ hs).2⟩

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