isClosed_image — Mathlib

English

A subset S of A is closed iff its image under a continuous algebra equivalence is closed.

Русский

Подмножество S ⊆ A замкнуто тогда и только тогда, когда его образ под непрерывной эквивалентностью замкнут.

LaTeX

$$$ IsClosed (e''S) \iff IsClosed(S) $$$

Lean4

@[simp]
theorem isClosed_image (e : A ≃A[R] B) {S : Set A} : IsClosed (e '' S) ↔ IsClosed S :=
  e.toHomeomorph.isClosed_image

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