isPreirreducible_iff_closure — Mathlib

English

IsPreirreducible is preserved by closure: IsPreirreducible(closure s) iff IsPreirreducible(s).

Русский

Неразложимость сохраняется при замыкании: IsPreirreducible(closure s) ⇔ IsPreirreducible(s).

LaTeX

$$$\\operatorname{IsPreirreducible}(\\overline{s}) \\iff \\operatorname{IsPreirreducible}(s)$$$

Lean4

theorem isPreirreducible_iff_closure : IsPreirreducible (closure s) ↔ IsPreirreducible s :=
  forall₄_congr fun u v hu hv => by
    iterate 3 rw [closure_inter_open_nonempty_iff]
    exacts [hu.inter hv, hv, hu]

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