alexandrovDiscrete_coinduced — Mathlib

English

For any β and any f: α → β, the coinduced topology on β makes β Alexandrov-discrete if α is Alexandrov-discrete.

Русский

Пусть β произвольное, а f: α → β; тогда сопряженная (coinduced) топология на β делает β Александрово-дискретным при условии, что α Александрово-дискретно.

LaTeX

$$AlexandrovDiscrete β (coinduced f α)$$

Lean4

theorem alexandrovDiscrete_coinduced {β : Type*} {f : α → β} : @AlexandrovDiscrete β (coinduced f ‹_›) :=
  @AlexandrovDiscrete.mk β (coinduced f ‹_›) fun S hS ↦ by rw [isOpen_coinduced, preimage_sInter];
    exact isOpen_iInter₂ hS

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