case intro
α : Type ?u.37481
X : Type u_1
Y : Type ?u.37487
Z : Type ?u.37490
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S A B : DiscreteQuotient X
h : A ≤ B
a : X
⊢ proj A ⁻¹' {proj A a} ⊆ proj B ⁻¹' {ofLE h (proj A a)}
α : Type ?u.37481
X : Type u_1
Y : Type ?u.37487
Z : Type ?u.37490
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S A B : DiscreteQuotient X
h : A ≤ B
a : Quotient A.toSetoid
⊢ proj A ⁻¹' {a} ⊆ proj B ⁻¹' {ofLE h a}
rcases A.proj_surjective a with ⟨a, rfl⟩
case intro
α : Type ?u.37481
X : Type u_1
Y : Type ?u.37487
Z : Type ?u.37490
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S A B : DiscreteQuotient X
h : A ≤ B
a : X
⊢ setOf (Setoid.Rel A.toSetoid a) ⊆ setOf (Setoid.Rel B.toSetoid a)
case intro
α : Type ?u.37481
X : Type u_1
Y : Type ?u.37487
Z : Type ?u.37490
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S A B : DiscreteQuotient X
h : A ≤ B
a : X
⊢ proj A ⁻¹' {proj A a} ⊆ proj B ⁻¹' {ofLE h (proj A a)}
rw [fiber_eq, ofLE_proj, fiber_eq]
no goals
case intro
α : Type ?u.37481
X : Type u_1
Y : Type ?u.37487
Z : Type ?u.37490
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S A B : DiscreteQuotient X
h : A ≤ B
a : X
⊢ setOf (Setoid.Rel A.toSetoid a) ⊆ setOf (Setoid.Rel B.toSetoid a)
exact fun _ h' => h h'