fundCircuit_eq_sInter — Mathlib

English

The fundamental circuit equals the inserted element together with the intersection of certain closures; more precisely, it equals insert e of I intersected with a certain sInter construction.

Русский

Фундокруг равен вставке e в I, пересеченной с определённой конструкцией sInter.

LaTeX

$$$M.fundCircuit\ e\ I = \text{insert } e ( I \cap \bigcap_0\{J\subset I \mid e\in \overline{J}\})$$$

Lean4

theorem fundCircuit_eq_sInter (he : e ∈ M.closure I) :
    M.fundCircuit e I = insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J}) :=
  by
  rw [fundCircuit]
  simp_rw [closure_subset_closure_iff_subset_closure (show { e } ⊆ M.E by simpa using mem_ground_of_mem_closure he),
    singleton_subset_iff]
  rw [inter_eq_self_of_subset_right (sInter_subset_of_mem (by simpa))]

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