preirreducibleSpace — Mathlib

English

If s is preirreducible, then the subspace s with the ambient topology is preirreducible.

Русский

Если s преднеразложимо, то подпространство s с вложенной топологией преднеразложимо.

LaTeX

$$$\mathrm{IsPreirreducible}(s) \rightarrow \mathrm{PreirreducibleSpace}(s)$$$

Lean4

theorem preirreducibleSpace (h : IsPreirreducible s) : PreirreducibleSpace s where
  isPreirreducible_univ :=
    by
    rintro _ _ ⟨u, hu, rfl⟩ ⟨v, hv, rfl⟩ ⟨⟨x, hxs⟩, -, hxu⟩ ⟨⟨y, hys⟩, -, hyv⟩
    rcases h u v hu hv ⟨x, hxs, hxu⟩ ⟨y, hys, hyv⟩ with ⟨x, hxs, ⟨hxu, hxv⟩⟩
    exact ⟨⟨x, hxs⟩, ⟨Set.mem_univ _, ⟨hxu, hxv⟩⟩⟩

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