English
Irreducibility of s is equivalent to a finite sInter criterion: for every finite collection of open sets, if s meets each, then s meets their intersection.
Русский
Неразложимость s эквивалентна конечной характеристике: для любой конечной коллекции открытых множеств, если s пересекает каждое из них, то s пересекает их пересечение.
LaTeX
$$$\mathrm{IsIrreducible}(s) \iff \forall U \in \mathrm{Finset}(\mathcal{P}(X)), \big( \forall u \in U, \mathrm{IsOpen}(u) \big) \to \big( \forall u \in U, (s \cap u) \neq \varnothing \big) \to \big( s \cap \bigcap U \big) \neq \varnothing$$$
Lean4
/-- A set `s` is irreducible if and only if
for every finite collection of open sets all of whose members intersect `s`,
`s` also intersects the intersection of the entire collection
(i.e., there is an element of `s` contained in every member of the collection). -/
theorem isIrreducible_iff_sInter :
IsIrreducible s ↔
∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty :=
by
classical
refine ⟨fun h U hu hU => ?_, fun h => ⟨?_, ?_⟩⟩
·
induction U using Finset.induction_on with
| empty => simpa using h.nonempty
| insert u U _ IH =>
rw [Finset.coe_insert, sInter_insert]
rw [Finset.forall_mem_insert] at hu hU
exact h.2 _ _ hu.1 (U.finite_toSet.isOpen_sInter hu.2) hU.1 (IH hu.2 hU.2)
· simpa using h ∅
· intro u v hu hv hu' hv'
simpa [*] using h { u, v }
