α : Type u
β : Type v
γ : Type w
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
⊢ induced f inst✝¹ ≤ Preorder.topology α
α : Type u
β : Type v
γ : Type w
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
⊢ induced f inst✝¹ ≤ Preorder.topology α
let _ := Preorder.topology α
α : Type u
β : Type v
γ : Type w
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ induced f inst✝¹ ≤ Preorder.topology α
α : Type u
β : Type v
γ : Type w
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
⊢ induced f inst✝¹ ≤ Preorder.topology α
have : OrderTopology α := ⟨rfl⟩
α : Type u
β : Type v
γ : Type w
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
x : α
⊢ 𝓝 x ≤ 𝓝 x
α : Type u
β : Type v
γ : Type w
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ induced f inst✝¹ ≤ Preorder.topology α
refine le_of_nhds_le_nhds fun x => ?_
α : Type u
β : Type v
γ : Type w
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
x : α
⊢ ((⨅ (i : β) (_ : i ∈ {x_1 | x_1 < f x}), 𝓟 (f ⁻¹' {x | i < x})) ⊓
      ⨅ (i : β) (_ : i ∈ {x_1 | f x < x_1}), 𝓟 (f ⁻¹' {x | x < i})) ≤
    (⨅ (b : α) (_ : b ∈ {x_1 | f x_1 < f x}), 𝓟 {x | f b < f x}) ⊓
      ⨅ (b : α) (_ : b ∈ {x_1 | f x < f x_1}), 𝓟 {x | f x < f b}
α : Type u
β : Type v
γ : Type w
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
x : α
⊢ 𝓝 x ≤ 𝓝 x
simp only [nhds_eq_order, nhds_induced, comap_inf, comap_iInf, comap_principal, Ioi, Iio, ← hf]
case refine_1
α : Type u
β : Type v
γ : Type w
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
x a : α
ha : a ∈ {x_1 | f x_1 < f x}
⊢ (⨅ (i : β) (_ : i ∈ {x_1 | x_1 < f x}), 𝓟 (f ⁻¹' {x | i < x})) ≤ 𝓟 {x | f a < f x}

case refine_2
α : Type u
β : Type v
γ : Type w
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
x a : α
ha : a ∈ {x_1 | f x < f x_1}
⊢ (⨅ (i : β) (_ : i ∈ {x_1 | f x < x_1}), 𝓟 (f ⁻¹' {x | x < i})) ≤ 𝓟 {x | f x < f a}
α : Type u
β : Type v
γ : Type w
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
x : α
⊢ ((⨅ (i : β) (_ : i ∈ {x_1 | x_1 < f x}), 𝓟 (f ⁻¹' {x | i < x})) ⊓
      ⨅ (i : β) (_ : i ∈ {x_1 | f x < x_1}), 𝓟 (f ⁻¹' {x | x < i})) ≤
    (⨅ (b : α) (_ : b ∈ {x_1 | f x_1 < f x}), 𝓟 {x | f b < f x}) ⊓
      ⨅ (b : α) (_ : b ∈ {x_1 | f x < f x_1}), 𝓟 {x | f x < f b}
refine inf_le_inf (le_iInf₂ fun a ha => ?_) (le_iInf₂ fun a ha => ?_)
no goals
case refine_1
α : Type u
β : Type v
γ : Type w
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
x a : α
ha : a ∈ {x_1 | f x_1 < f x}
⊢ (⨅ (i : β) (_ : i ∈ {x_1 | x_1 < f x}), 𝓟 (f ⁻¹' {x | i < x})) ≤ 𝓟 {x | f a < f x}

case refine_2
α : Type u
β : Type v
γ : Type w
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
x a : α
ha : a ∈ {x_1 | f x < f x_1}
⊢ (⨅ (i : β) (_ : i ∈ {x_1 | f x < x_1}), 𝓟 (f ⁻¹' {x | x < i})) ≤ 𝓟 {x | f x < f a}
exacts [iInf₂_le (f a) ha, iInf₂_le (f a) ha]