Theorems · Theorem · general topology

IsExtrOn.comp_mapsTo

∀ {α : Type u} {β : Type v} {δ : Type x} [inst : Preorder β] {f : α → β} {s : Set α} {a : α} {t : Set δ} {g : δ → α}
  {b : δ}, IsExtrOn f s a → Set.MapsTo g t s → g b = a → IsExtrOn (f ∘ g) t b

Defined in

Mathlib.Order.Filter.Extr

Cited by

0 results in Mathlib

Foundations

Depth 17 from the axioms · uses Quot.sound

Assumes

Preorder