α : Type ?u.38375
X : Type u_1
Y : Type ?u.38381
Z : Type ?u.38384
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
H₁ : ∀ (Q₁ Q₂ : DiscreteQuotient X), Q₁ ≤ Q₂ → proj Q₁ ⁻¹' {Qs Q₁} ⊆ proj Q₂ ⁻¹' {Qs Q₂}
⊢ ∃ x, ∀ (Q : DiscreteQuotient X), proj Q x = Qs Q
α : Type ?u.38375
X : Type u_1
Y : Type ?u.38381
Z : Type ?u.38384
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
⊢ ∃ x, ∀ (Q : DiscreteQuotient X), proj Q x = Qs Q
have H₁ : ∀ Q₁ Q₂, Q₁ ≤ Q₂ → proj Q₁ ⁻¹' {Qs Q₁} ⊆ proj Q₂ ⁻¹' {Qs Q₂} := fun _ _ h => by
  rw [← compat _ _ h]
  exact fiber_subset_ofLE _ _
case intro
α : Type ?u.38375
X : Type u_1
Y : Type ?u.38381
Z : Type ?u.38384
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
H₁ : ∀ (Q₁ Q₂ : DiscreteQuotient X), Q₁ ≤ Q₂ → proj Q₁ ⁻¹' {Qs Q₁} ⊆ proj Q₂ ⁻¹' {Qs Q₂}
x : X
hx : x ∈ ⋂ (Q : DiscreteQuotient X), proj Q ⁻¹' {Qs Q}
⊢ ∃ x, ∀ (Q : DiscreteQuotient X), proj Q x = Qs Q
α : Type ?u.38375
X : Type u_1
Y : Type ?u.38381
Z : Type ?u.38384
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
H₁ : ∀ (Q₁ Q₂ : DiscreteQuotient X), Q₁ ≤ Q₂ → proj Q₁ ⁻¹' {Qs Q₁} ⊆ proj Q₂ ⁻¹' {Qs Q₂}
⊢ ∃ x, ∀ (Q : DiscreteQuotient X), proj Q x = Qs Q
obtain ⟨x, hx⟩ : Set.Nonempty (⋂ Q, proj Q ⁻¹' {Qs Q}) :=
  IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed
    (fun Q : DiscreteQuotient X => Q.proj ⁻¹' {Qs _}) (directed_of_inf H₁)
    (fun Q => (singleton_nonempty _).preimage Q.proj_surjective)
    (fun Q => (Q.isClosed_preimage {Qs _}).isCompact) fun Q => Q.isClosed_preimage _
no goals
case intro
α : Type ?u.38375
X : Type u_1
Y : Type ?u.38381
Z : Type ?u.38384
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
H₁ : ∀ (Q₁ Q₂ : DiscreteQuotient X), Q₁ ≤ Q₂ → proj Q₁ ⁻¹' {Qs Q₁} ⊆ proj Q₂ ⁻¹' {Qs Q₂}
x : X
hx : x ∈ ⋂ (Q : DiscreteQuotient X), proj Q ⁻¹' {Qs Q}
⊢ ∃ x, ∀ (Q : DiscreteQuotient X), proj Q x = Qs Q
exact ⟨x, mem_iInter.1 hx⟩
α : Type ?u.38375
X : Type u_1
Y : Type ?u.38381
Z : Type ?u.38384
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
x✝¹ x✝ : DiscreteQuotient X
h : x✝¹ ≤ x✝
⊢ proj x✝¹ ⁻¹' {Qs x✝¹} ⊆ proj x✝ ⁻¹' {ofLE h (Qs x✝¹)}
α : Type ?u.38375
X : Type u_1
Y : Type ?u.38381
Z : Type ?u.38384
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
x✝¹ x✝ : DiscreteQuotient X
h : x✝¹ ≤ x✝
⊢ proj x✝¹ ⁻¹' {Qs x✝¹} ⊆ proj x✝ ⁻¹' {Qs x✝}
rw [← compat _ _ h]
no goals
α : Type ?u.38375
X : Type u_1
Y : Type ?u.38381
Z : Type ?u.38384
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
x✝¹ x✝ : DiscreteQuotient X
h : x✝¹ ≤ x✝
⊢ proj x✝¹ ⁻¹' {Qs x✝¹} ⊆ proj x✝ ⁻¹' {ofLE h (Qs x✝¹)}
exact fiber_subset_ofLE _ _