Theorem: QuasiconcaveOn.antitone_comp (Sion/Concavexity.lean)

State before:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Antitone g
hf : QuasiconcaveOn 𝕜 s f
⊢ QuasiconvexOn 𝕜 s (g ∘ f)
Tactic:
apply QuasiconvexOn.antitone_comp (β := βᵒᵈ) (γ := γᵒᵈ) (f := f) _ hf
State after:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Antitone g
hf : QuasiconcaveOn 𝕜 s f
⊢ Antitone g

State before:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Antitone g
hf : QuasiconcaveOn 𝕜 s f
⊢ Antitone g
Tactic:
rw [← antitone_dual_iff]
State after:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Antitone g
hf : QuasiconcaveOn 𝕜 s f
⊢ Antitone (⇑OrderDual.toDual ∘ g ∘ ⇑OrderDual.ofDual)

State before:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Antitone g
hf : QuasiconcaveOn 𝕜 s f
⊢ Antitone (⇑OrderDual.toDual ∘ g ∘ ⇑OrderDual.ofDual)
Tactic:
exact hg
State after:
no goals