exists_gt — Mathlib

English

Let s be a closed subset of a topological space X, and v be a partial refinement indexed by ι with carrier not containing i. Then there exists a strictly larger partial refinement v′ with v < v′.

Русский

Пусть S — замкнутое подмножество т.с., и v — частичное уточнение, индексированное по ι, причём i не лежит в носителе v. Тогда существует строго большее частичное уточнение v′ с v < v′.

LaTeX

$$$\text{Let } s \subseteq X \text{ be closed. Let } v \in \text{PartialRefinement}(u,s)_{\top}.\text{ If } i \notin v_{carrier}, \text{ then } \exists v'\, (v < v').$$$

Lean4

/-- If `s` is a closed set, `v` is a partial refinement, and `i` is an index such that
`i ∉ v.carrier`, then there exists a partial refinement that is strictly greater than `v`. -/
theorem exists_gt [NormalSpace X] (v : PartialRefinement u s ⊤) (hs : IsClosed s) (i : ι) (hi : i ∉ v.carrier) :
    ∃ v' : PartialRefinement u s ⊤, v < v' :=
  by
  have I : (s ∩ ⋂ (j) (_ : j ≠ i), (v j)ᶜ) ⊆ v i :=
    by
    simp only [subset_def, mem_inter_iff, mem_iInter, and_imp]
    intro x hxs H
    rcases mem_iUnion.1 (v.subset_iUnion hxs) with ⟨j, hj⟩
    exact (em (j = i)).elim (fun h => h ▸ hj) fun h => (H j h hj).elim
  have C : IsClosed (s ∩ ⋂ (j) (_ : j ≠ i), (v j)ᶜ) :=
    IsClosed.inter hs (isClosed_biInter fun _ _ => isClosed_compl_iff.2 <| v.isOpen _)
  rcases normal_exists_closure_subset C (v.isOpen i) I with ⟨vi, ovi, hvi, cvi⟩
  classical
  refine ⟨⟨update v i vi, insert i v.carrier, ?_, ?_, ?_, ?_, ?_⟩, ?_, ?_⟩
  · intro j
    rcases eq_or_ne j i with (rfl | hne) <;> simp [*, v.isOpen]
  · refine fun x hx => mem_iUnion.2 ?_
    rcases em (∃ j ≠ i, x ∈ v j) with (⟨j, hji, hj⟩ | h)
    · use j
      rwa [update_of_ne hji]
    · push_neg at h
      use i
      rw [update_self]
      exact hvi ⟨hx, mem_biInter h⟩
  · rintro j (rfl | hj)
    · rwa [update_self, ← v.apply_eq hi]
    · rw [update_of_ne (ne_of_mem_of_not_mem hj hi)]
      exact v.closure_subset hj
  · exact fun _ => trivial
  · intro j hj
    rw [mem_insert_iff, not_or] at hj
    rw [update_of_ne hj.1, v.apply_eq hj.2]
  · refine ⟨subset_insert _ _, fun j hj => ?_⟩
    exact (update_of_ne (ne_of_mem_of_not_mem hj hi) _ _).symm
  · exact fun hle => hi (hle.1 <| mem_insert _ _)

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