finiteInterClosure_insert — Mathlib

English

If P lies in finiteInterClosure(insert A S), then P ∈ S or there exists Q ∈ S with P = A ∩ Q.

Русский

Если P лежит в конечном замыкании по вставке, то 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 finiteInterClosure_insert {A : Set α} (cond : FiniteInter S) (P) (H : P ∈ finiteInterClosure (insert A S)) :
    P ∈ S ∨ ∃ Q ∈ S, P = A ∩ Q := by
  induction H with
  | basic h =>
    cases h
    · exact Or.inr ⟨Set.univ, cond.univ_mem, by simpa⟩
    · exact Or.inl (by assumption)
  | univ => exact Or.inl cond.univ_mem
  | @inter T1 T2 _ _ h1
    h2 =>
    rcases h1 with (h | ⟨Q, hQ, rfl⟩) <;> rcases h2 with (i | ⟨R, hR, rfl⟩)
    · exact Or.inl (cond.inter_mem h i)
    · exact Or.inr ⟨T1 ∩ R, cond.inter_mem h hR, by simp only [← Set.inter_assoc, Set.inter_comm _ A]⟩
    · exact Or.inr ⟨Q ∩ T2, cond.inter_mem hQ i, by simp only [Set.inter_assoc]⟩
    ·
      exact
        Or.inr
          ⟨Q ∩ R, cond.inter_mem hQ hR, by
            ext x
            constructor <;> simp +contextual⟩

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