finiteInter_mem — Mathlib

English

If P ∈ finiteInterClosure (insert A S), then P ∈ S or ∃ Q ∈ S, P = A ∩ Q.

Русский

Если P ∈ finiteInterClosure (insert A S), то P ∈ S или существует Q ∈ S, P = A ∩ Q.

LaTeX

$$$P \in \operatorname{finiteInterClosure}(\operatorname{insert} A S) \Rightarrow P \in S \lor \exists Q \in S, P = A \cap Q$$$

Lean4

theorem finiteInter_mem (cond : FiniteInter S) (F : Finset (Set α)) : ↑F ⊆ S → ⋂₀ (↑F : Set (Set α)) ∈ S := by
  classical
  refine Finset.induction_on F (fun _ => ?_) ?_
  · simp [cond.univ_mem]
  · intro a s _ h1 h2
    suffices a ∩ ⋂₀ ↑s ∈ S by simpa
    exact cond.inter_mem (h2 (Finset.mem_insert_self a s)) (h1 fun x hx => h2 <| Finset.mem_insert_of_mem hx)

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