case h
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.39096
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x✝ x : E
⊢ x ∈ vertices K ↔ x ∈ ⋃ (k : Finset E) (_ : k ∈ K.faces), ↑k
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.39096
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
⊢ vertices K = ⋃ (k : Finset E) (_ : k ∈ K.faces), ↑k
ext x
case h
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.39096
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x✝ x : E
h : x ∈ ⋃ (k : Finset E) (_ : k ∈ K.faces), ↑k
⊢ x ∈ vertices K
case h
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.39096
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x✝ x : E
⊢ x ∈ vertices K ↔ x ∈ ⋃ (k : Finset E) (_ : k ∈ K.faces), ↑k
refine' ⟨fun h => mem_biUnion h <| mem_coe.2 <| mem_singleton_self x, fun h => _⟩
case h.intro.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.39096
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s✝ t : Finset E
x✝ x : E
h : x ∈ ⋃ (k : Finset E) (_ : k ∈ K.faces), ↑k
s : Finset E
hs : s ∈ K.faces
hx : x ∈ ↑s
⊢ x ∈ vertices K
case h
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.39096
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x✝ x : E
h : x ∈ ⋃ (k : Finset E) (_ : k ∈ K.faces), ↑k
⊢ x ∈ vertices K
obtain ⟨s, hs, hx⟩ := mem_iUnion₂.1 h
no goals
case h.intro.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.39096
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s✝ t : Finset E
x✝ x : E
h : x ∈ ⋃ (k : Finset E) (_ : k ∈ K.faces), ↑k
s : Finset E
hs : s ∈ K.faces
hx : x ∈ ↑s
⊢ x ∈ vertices K
exact K.down_closed hs (Finset.singleton_subset_iff.2 <| mem_coe.1 hx) (singleton_ne_empty _)