Theorem: Convex.quasiconcaveOn_restrict (Sion/Concavexity.lean)

State before:
𝕜 : Type u_3
E : Type u_1
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type u_2
inst✝ : Preorder β
s : Set E
f : E → β
t : Set E
hf : QuasiconcaveOn 𝕜 s f
hst : t ⊆ s
ht : Convex 𝕜 t
⊢ QuasiconcaveOn 𝕜 t f
Tactic:
intro b
State after:
𝕜 : Type u_3
E : Type u_1
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type u_2
inst✝ : Preorder β
s : Set E
f : E → β
t : Set E
hf : QuasiconcaveOn 𝕜 s f
hst : t ⊆ s
ht : Convex 𝕜 t
b : β
⊢ Convex 𝕜 {x | x ∈ t ∧ b ≤ f x}

State before:
𝕜 : Type u_3
E : Type u_1
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type u_2
inst✝ : Preorder β
s : Set E
f : E → β
t : Set E
hf : QuasiconcaveOn 𝕜 s f
hst : t ⊆ s
ht : Convex 𝕜 t
b : β
⊢ Convex 𝕜 {x | x ∈ t ∧ b ≤ f x}
Tactic:
rw [Set.sep_of_subset hst]
State after:
𝕜 : Type u_3
E : Type u_1
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type u_2
inst✝ : Preorder β
s : Set E
f : E → β
t : Set E
hf : QuasiconcaveOn 𝕜 s f
hst : t ⊆ s
ht : Convex 𝕜 t
b : β
⊢ Convex 𝕜 ({x | x ∈ s ∧ b ≤ f x} ∩ t)

State before:
𝕜 : Type u_3
E : Type u_1
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type u_2
inst✝ : Preorder β
s : Set E
f : E → β
t : Set E
hf : QuasiconcaveOn 𝕜 s f
hst : t ⊆ s
ht : Convex 𝕜 t
b : β
⊢ Convex 𝕜 ({x | x ∈ s ∧ b ≤ f x} ∩ t)
Tactic:
exact Convex.inter (hf b) ht
State after:
no goals