Theorem: Geometry.SimplicialComplex.combiInteriors_partition (LeanCamCombi/SimplicialComplex/Basic.lean)

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hx : x ∈ K.space
⊢ ∃! s, s ∈ K ∧ x ∈ combiInterior 𝕜 s
Tactic:
rw [← combiInteriors_cover] at hx
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hx : x ∈ ⋃ s ∈ K, combiInterior 𝕜 s
⊢ ∃! s, s ∈ K ∧ x ∈ combiInterior 𝕜 s

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hx : x ∈ ⋃ s ∈ K, combiInterior 𝕜 s
⊢ ∃! s, s ∈ K ∧ x ∈ combiInterior 𝕜 s
Tactic:
obtain ⟨s, hs, hxs⟩ := Set.mem_iUnion₂.1 hx
State after:
case intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
hx : x ∈ ⋃ s ∈ K, combiInterior 𝕜 s
s : Finset E
hs : s ∈ K
hxs : x ∈ combiInterior 𝕜 s
⊢ ∃! s, s ∈ K ∧ x ∈ combiInterior 𝕜 s

State before:
case intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
hx : x ∈ ⋃ s ∈ K, combiInterior 𝕜 s
s : Finset E
hs : s ∈ K
hxs : x ∈ combiInterior 𝕜 s
⊢ ∃! s, s ∈ K ∧ x ∈ combiInterior 𝕜 s
Tactic:
exact ⟨s, ⟨⟨hs, hxs⟩, fun t ⟨ht, hxt⟩ => disjoint_interiors ht hs hxt hxs⟩⟩
State after:
no goals