English
If F is a nonempty finite collection of subsets of E and every member B ∈ F is exposed with respect to A, then the intersection of all sets in F, denoted ⋂₀F, is exposed with respect to A.
Русский
Если F — непустое конечное семейство подмножеств E и каждый элемент B ∈ F экспонирован относительно A, то пересечение ⋂₀F экспонировано относительно A.
LaTeX
$$$$ F \text{ nonempty} \;\land\; (\forall B \in F,\ IsExposed\ 𝕜\ A\ B) \Rightarrow IsExposed\ 𝕜\ A\ (\bigcap_{B \in F} B). $$$$
Lean4
theorem sInter [IsOrderedRing 𝕜] [ContinuousAdd 𝕜] {F : Finset (Set E)} (hF : F.Nonempty)
(hAF : ∀ B ∈ F, IsExposed 𝕜 A B) : IsExposed 𝕜 A (⋂₀ F) := by
classical
induction F using Finset.induction with
| empty => exfalso; exact Finset.not_nonempty_empty hF
| insert C F _ hF' =>
rw [Finset.coe_insert, sInter_insert]
obtain rfl | hFnemp := F.eq_empty_or_nonempty
· rw [Finset.coe_empty, sInter_empty, inter_univ]
exact hAF C (Finset.mem_singleton_self C)
· exact (hAF C (Finset.mem_insert_self C F)).inter (hF' hFnemp fun B hB => hAF B (Finset.mem_insert_of_mem hB))
