English
Assume X is compact and Qs assigns to each discrete quotient Q a value Qs(Q) in Q, with a compatibility condition: for all A ≤ B, ofLE h (Qs A) = Qs B. Then there exists x ∈ X such that for every quotient Q, Q.proj x = Qs Q.
Русский
Пусть X компактно, Qs задаёт каждому дискретному фактору Q элемент Qs(Q) в Q, и существуют совместимости: при любых A ≤ B выполняется ofLE h (Qs A) = Qs B. Тогда существует x ∈ X такой, что для каждого Q выполняется Q.proj x = Qs Q.
LaTeX
$$$\\exists x:\\, X, \\forall Q:\\, \\mathrm{DiscreteQuotient}\\, X,\\; Q.proj(x) = Qs(Q)$$$
Lean4
theorem exists_of_compat [CompactSpace X] (Qs : (Q : DiscreteQuotient X) → Q)
(compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs _) = Qs _) :
∃ x : X, ∀ Q : DiscreteQuotient X, Q.proj x = Qs _ :=
by
have H₁ : ∀ Q₁ Q₂, Q₁ ≤ Q₂ → proj Q₁ ⁻¹' {Qs Q₁} ⊆ proj Q₂ ⁻¹' {Qs Q₂} := fun _ _ h =>
by
rw [← compat _ _ h]
exact fiber_subset_ofLE _ _
obtain ⟨x, hx⟩ : Set.Nonempty (⋂ Q, proj Q ⁻¹' {Qs Q}) :=
IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed (fun Q : DiscreteQuotient X => Q.proj ⁻¹' {Qs _})
(directed_of_isDirected_ge H₁) (fun Q => (singleton_nonempty _).preimage Q.proj_surjective)
(fun Q => (Q.isClosed_preimage {Qs _}).isCompact) fun Q => Q.isClosed_preimage _
exact ⟨x, mem_iInter.1 hx⟩
