iInter — Mathlib

English

An indexed intersection of blocks is a block: iInter of a family of blocks is a block.

Русский

Неиндексированное пересечение блоков является блоком: пересечение по индексу — блок.

LaTeX

$$$ \\text{IsBlock } G (\\bigcap_{i} B(i)). $$$

Lean4

/-- An intersection of blocks is a block. -/
@[to_additive /-- An intersection of blocks is a block. -/
    ]
theorem iInter {ι : Sort*} {B : ι → Set X} (hB : ∀ i, IsBlock G (B i)) : IsBlock G (⋂ i, B i) :=
  by
  simp only [isBlock_iff_smul_eq_smul_of_nonempty, smul_set_iInter] at hB ⊢
  rintro g₁ g₂ ⟨a, ha₁, ha₂⟩
  simp_rw [fun i ↦ hB i ⟨a, iInter_subset _ i ha₁, iInter_subset _ i ha₂⟩]

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