Theorems · Theorem · general topology

Filter.comap_embedding_atTop

∀ {β : Type u_4} {γ : Type u_5} [inst : Preorder β] [inst_1 : Preorder γ] {e : β → γ},
  (∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂) → (∀ (c : γ), ∃ b, c ≤ e b) → Filter.comap e Filter.atTop = Filter.atTop

Defined in

Mathlib.Order.Filter.AtTopBot.Tendsto

Cited by

4 results in Mathlib

Foundations

Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PreorderPreorder