case empty.h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : E →L[𝕜] 𝕜
A B C : Set E
X : Finset E
x : E
inst✝ : ContinuousAdd 𝕜
hF : Finset.Nonempty ∅
hAF : ∀ (B : Set E), B ∈ ∅ → IsExposed 𝕜 A B
⊢ False
case empty
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : E →L[𝕜] 𝕜
A B C : Set E
X : Finset E
x : E
inst✝ : ContinuousAdd 𝕜
hF : Finset.Nonempty ∅
hAF : ∀ (B : Set E), B ∈ ∅ → IsExposed 𝕜 A B
⊢ IsExposed 𝕜 A (⋂₀ ↑∅)
exfalso
no goals
case empty.h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : E →L[𝕜] 𝕜
A B C : Set E
X : Finset E
x : E
inst✝ : ContinuousAdd 𝕜
hF : Finset.Nonempty ∅
hAF : ∀ (B : Set E), B ∈ ∅ → IsExposed 𝕜 A B
⊢ False
exact Finset.not_nonempty_empty hF
case insert
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : E →L[𝕜] 𝕜
A B C✝ : Set E
X : Finset E
x : E
inst✝ : ContinuousAdd 𝕜
C : Set E
F : Finset (Set E)
a✝ : ¬C ∈ F
hF' : Finset.Nonempty F → (∀ (B : Set E), B ∈ F → IsExposed 𝕜 A B) → IsExposed 𝕜 A (⋂₀ ↑F)
hF : Finset.Nonempty (insert C F)
hAF : ∀ (B : Set E), B ∈ insert C F → IsExposed 𝕜 A B
⊢ IsExposed 𝕜 A (C ∩ ⋂₀ ↑F)
case insert
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : E →L[𝕜] 𝕜
A B C✝ : Set E
X : Finset E
x : E
inst✝ : ContinuousAdd 𝕜
C : Set E
F : Finset (Set E)
a✝ : ¬C ∈ F
hF' : Finset.Nonempty F → (∀ (B : Set E), B ∈ F → IsExposed 𝕜 A B) → IsExposed 𝕜 A (⋂₀ ↑F)
hF : Finset.Nonempty (insert C F)
hAF : ∀ (B : Set E), B ∈ insert C F → IsExposed 𝕜 A B
⊢ IsExposed 𝕜 A (⋂₀ ↑(insert C F))
rw [Finset.coe_insert, sInter_insert]
case insert.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : E →L[𝕜] 𝕜
A B C✝ : Set E
X : Finset E
x : E
inst✝ : ContinuousAdd 𝕜
C : Set E
a✝ : ¬C ∈ ∅
hF' : Finset.Nonempty ∅ → (∀ (B : Set E), B ∈ ∅ → IsExposed 𝕜 A B) → IsExposed 𝕜 A (⋂₀ ↑∅)
hF : Finset.Nonempty (insert C ∅)
hAF : ∀ (B : Set E), B ∈ insert C ∅ → IsExposed 𝕜 A B
⊢ IsExposed 𝕜 A (C ∩ ⋂₀ ↑∅)

case insert.inr
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : E →L[𝕜] 𝕜
A B C✝ : Set E
X : Finset E
x : E
inst✝ : ContinuousAdd 𝕜
C : Set E
F : Finset (Set E)
a✝ : ¬C ∈ F
hF' : Finset.Nonempty F → (∀ (B : Set E), B ∈ F → IsExposed 𝕜 A B) → IsExposed 𝕜 A (⋂₀ ↑F)
hF : Finset.Nonempty (insert C F)
hAF : ∀ (B : Set E), B ∈ insert C F → IsExposed 𝕜 A B
hFnemp : Finset.Nonempty F
⊢ IsExposed 𝕜 A (C ∩ ⋂₀ ↑F)
case insert
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : E →L[𝕜] 𝕜
A B C✝ : Set E
X : Finset E
x : E
inst✝ : ContinuousAdd 𝕜
C : Set E
F : Finset (Set E)
a✝ : ¬C ∈ F
hF' : Finset.Nonempty F → (∀ (B : Set E), B ∈ F → IsExposed 𝕜 A B) → IsExposed 𝕜 A (⋂₀ ↑F)
hF : Finset.Nonempty (insert C F)
hAF : ∀ (B : Set E), B ∈ insert C F → IsExposed 𝕜 A B
⊢ IsExposed 𝕜 A (C ∩ ⋂₀ ↑F)
obtain rfl | hFnemp := F.eq_empty_or_nonempty
case insert.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : E →L[𝕜] 𝕜
A B C✝ : Set E
X : Finset E
x : E
inst✝ : ContinuousAdd 𝕜
C : Set E
a✝ : ¬C ∈ ∅
hF' : Finset.Nonempty ∅ → (∀ (B : Set E), B ∈ ∅ → IsExposed 𝕜 A B) → IsExposed 𝕜 A (⋂₀ ↑∅)
hF : Finset.Nonempty (insert C ∅)
hAF : ∀ (B : Set E), B ∈ insert C ∅ → IsExposed 𝕜 A B
⊢ IsExposed 𝕜 A C
case insert.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : E →L[𝕜] 𝕜
A B C✝ : Set E
X : Finset E
x : E
inst✝ : ContinuousAdd 𝕜
C : Set E
a✝ : ¬C ∈ ∅
hF' : Finset.Nonempty ∅ → (∀ (B : Set E), B ∈ ∅ → IsExposed 𝕜 A B) → IsExposed 𝕜 A (⋂₀ ↑∅)
hF : Finset.Nonempty (insert C ∅)
hAF : ∀ (B : Set E), B ∈ insert C ∅ → IsExposed 𝕜 A B
⊢ IsExposed 𝕜 A (C ∩ ⋂₀ ↑∅)
rw [Finset.coe_empty, sInter_empty, inter_univ]
no goals
case insert.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : E →L[𝕜] 𝕜
A B C✝ : Set E
X : Finset E
x : E
inst✝ : ContinuousAdd 𝕜
C : Set E
a✝ : ¬C ∈ ∅
hF' : Finset.Nonempty ∅ → (∀ (B : Set E), B ∈ ∅ → IsExposed 𝕜 A B) → IsExposed 𝕜 A (⋂₀ ↑∅)
hF : Finset.Nonempty (insert C ∅)
hAF : ∀ (B : Set E), B ∈ insert C ∅ → IsExposed 𝕜 A B
⊢ IsExposed 𝕜 A C
exact hAF C (Finset.mem_singleton_self C)
no goals
case insert.inr
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : E →L[𝕜] 𝕜
A B C✝ : Set E
X : Finset E
x : E
inst✝ : ContinuousAdd 𝕜
C : Set E
F : Finset (Set E)
a✝ : ¬C ∈ F
hF' : Finset.Nonempty F → (∀ (B : Set E), B ∈ F → IsExposed 𝕜 A B) → IsExposed 𝕜 A (⋂₀ ↑F)
hF : Finset.Nonempty (insert C F)
hAF : ∀ (B : Set E), B ∈ insert C F → IsExposed 𝕜 A B
hFnemp : Finset.Nonempty F
⊢ IsExposed 𝕜 A (C ∩ ⋂₀ ↑F)
exact (hAF C (Finset.mem_insert_self C F)).inter
  (hF' hFnemp fun B hB => hAF B (Finset.mem_insert_of_mem hB))