English
If t is preirreducible and U is a nonempty open subset with U ⊆ S ⊆ t, then S is irreducible.
Русский
Если t преднеразложимо и существует непустое открытое подмножество U с U ⊆ S ⊆ t, то S неразложимо.
LaTeX
$$$\mathrm{IsPreirreducible}(t) \to U\text{ isOpen} \to U \neq \emptyset \to U \subseteq S \to S \subseteq t \to \mathrm{IsIrreducible}(S)$$$
Lean4
/-- If `∅ ≠ U ⊆ S ⊆ t` such that `U` is open and `t` is preirreducible, then `S` is irreducible. -/
theorem subset_irreducible {S U : Set X} (ht : IsPreirreducible t) (hU : U.Nonempty) (hU' : IsOpen U) (h₁ : U ⊆ S)
(h₂ : S ⊆ t) : IsIrreducible S := by
obtain ⟨z, hz⟩ := hU
replace ht : IsIrreducible t := ⟨⟨z, h₂ (h₁ hz)⟩, ht⟩
refine ⟨⟨z, h₁ hz⟩, ?_⟩
rintro u v hu hv ⟨x, hx, hx'⟩ ⟨y, hy, hy'⟩
classical
obtain ⟨x, -, hx'⟩ : Set.Nonempty (t ∩ ⋂₀ ↑({ U, u, v } : Finset (Set X))) :=
by
refine isIrreducible_iff_sInter.mp ht { U, u, v } ?_ ?_
· simp [*]
· intro U H
simp only [Finset.mem_insert, Finset.mem_singleton] at H
rcases H with (rfl | rfl | rfl)
exacts [⟨z, h₂ (h₁ hz), hz⟩, ⟨x, h₂ hx, hx'⟩, ⟨y, h₂ hy, hy'⟩]
replace hx' : x ∈ U ∧ x ∈ u ∧ x ∈ v := by simpa using hx'
exact ⟨x, h₁ hx'.1, hx'.2⟩
