𝕜 : Type u_1
E : Type ?u.63373
F : Type ?u.63376
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : LinearOrderedAddCommMonoid β
s : Set 𝕜
f : 𝕜 → β
hf : QuasilinearOn 𝕜 s f
⊢ ∀ (a : 𝕜), a ∈ s → ∀ (b : 𝕜), b ∈ s → ∀ (c : 𝕜), c ∈ s → c ∈ segment 𝕜 a b → f c ∈ uIcc (f a) (f b)
𝕜 : Type u_1
E : Type ?u.63373
F : Type ?u.63376
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : LinearOrderedAddCommMonoid β
s : Set 𝕜
f : 𝕜 → β
hf : QuasilinearOn 𝕜 s f
⊢ MonotoneOn f s ∨ AntitoneOn f s
simp_rw [monotoneOn_or_antitoneOn_iff_uIcc, ← segment_eq_uIcc]
𝕜 : Type u_1
E : Type ?u.63373
F : Type ?u.63376
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : LinearOrderedAddCommMonoid β
s : Set 𝕜
f : 𝕜 → β
hf : QuasilinearOn 𝕜 s f
a : 𝕜
ha : a ∈ s
b : 𝕜
hb : b ∈ s
c : 𝕜
x✝ : c ∈ s
h : c ∈ segment 𝕜 a b
⊢ f c ∈ uIcc (f a) (f b)
𝕜 : Type u_1
E : Type ?u.63373
F : Type ?u.63376
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : LinearOrderedAddCommMonoid β
s : Set 𝕜
f : 𝕜 → β
hf : QuasilinearOn 𝕜 s f
⊢ ∀ (a : 𝕜), a ∈ s → ∀ (b : 𝕜), b ∈ s → ∀ (c : 𝕜), c ∈ s → c ∈ segment 𝕜 a b → f c ∈ uIcc (f a) (f b)
rintro a ha b hb c _ h
no goals
𝕜 : Type u_1
E : Type ?u.63373
F : Type ?u.63376
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : LinearOrderedAddCommMonoid β
s : Set 𝕜
f : 𝕜 → β
hf : QuasilinearOn 𝕜 s f
a : 𝕜
ha : a ∈ s
b : 𝕜
hb : b ∈ s
c : 𝕜
x✝ : c ∈ s
h : c ∈ segment 𝕜 a b
⊢ f c ∈ uIcc (f a) (f b)
refine' ⟨((hf.2 _).segment_subset _ _ h).2, ((hf.1 _).segment_subset _ _ h).2⟩ <;> simp [*]