English
If x is a fibre element of a LocallyConstant function l: S→Y with S compact, then its fibre component is compact.
Русский
Если x — элемент фибры локально-константной функции l: S→Y при S компактном, то его компонент в волокне компактна.
LaTeX
$$$$\text{If }x\in\mathrm{Fiber}(l)\text{ with }S\text{ compact, then } x.\mathrm{val} \text{ is compact.}$$$$
Lean4
instance (x : Fiber l) : CompactSpace x.val := by
obtain ⟨y, hy⟩ := x.prop
rw [← isCompact_iff_compactSpace, ← hy]
exact (l.2.isClosed_fiber _).isCompact
