α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
⊢ Set.Countable {x | ∃ y, x ⋖ y}
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
⊢ Set.Countable {x | ∃ y, x ⋖ y}
nontriviality α
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
⊢ Set.Countable {x | ∃ y, x ⋖ y}
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
⊢ Set.Countable {x | ∃ y, x ⋖ y}
let s := { x : α | ∃ y, x ⋖ y }
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
this : ∀ (x : α), x ∈ s → ∃ y, x ⋖ y
⊢ Set.Countable {x | ∃ y, x ⋖ y}
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
⊢ Set.Countable {x | ∃ y, x ⋖ y}
have : ∀ x ∈ s, ∃ y, x ⋖ y := fun x => id
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
⊢ Set.Countable {x | ∃ y, x ⋖ y}
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
this : ∀ (x : α), x ∈ s → ∃ y, x ⋖ y
⊢ Set.Countable {x | ∃ y, x ⋖ y}
choose! y hy using this
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
⊢ Set.Countable {x | ∃ y, x ⋖ y}
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
⊢ Set.Countable {x | ∃ y, x ⋖ y}
have Hy : ∀ x z, x ∈ s → z < y x → z ≤ x := fun x z hx => (hy x hx).le_of_lt
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
H : ∀ (a : Set α), IsOpen a → Set.Countable {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a}
⊢ Set.Countable {x | ∃ y, x ⋖ y}

case H
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
⊢ ∀ (a : Set α), IsOpen a → Set.Countable {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a}
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
⊢ Set.Countable {x | ∃ y, x ⋖ y}
suffices H : ∀ a : Set α, IsOpen a → Set.Countable { x | x ∈ s ∧ x ∈ a ∧ y x ∉ a }
case H
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
⊢ Set.Countable {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a}
case H
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
⊢ ∀ (a : Set α), IsOpen a → Set.Countable {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a}
intro a ha
case H
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
H : Set.Countable {x | (x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a) ∧ ¬IsBot x}
⊢ Set.Countable {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a}

case H
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
⊢ Set.Countable {x | (x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a) ∧ ¬IsBot x}
case H
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
⊢ Set.Countable {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a}
suffices H : Set.Countable { x | (x ∈ s ∧ x ∈ a ∧ y x ∉ a) ∧ ¬IsBot x }
case H
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
⊢ Set.Countable {x | x ∈ {x | ∃ y, x ⋖ y} ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
case H
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
⊢ Set.Countable {x | (x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a) ∧ ¬IsBot x}
simp only [and_assoc]
case H
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
⊢ Set.Countable {x | x ∈ {x | ∃ y, x ⋖ y} ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
case H
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
⊢ Set.Countable {x | x ∈ {x | ∃ y, x ⋖ y} ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
let t := { x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x }
case H
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
this : ∀ (x : α), x ∈ t → ∃ z, z < x ∧ Ioc z x ⊆ a
⊢ Set.Countable {x | x ∈ {x | ∃ y, x ⋖ y} ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
case H
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
⊢ Set.Countable {x | x ∈ {x | ∃ y, x ⋖ y} ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
have : ∀ x ∈ t, ∃ z < x, Ioc z x ⊆ a := by
  intro x hx
  apply exists_Ioc_subset_of_mem_nhds (ha.mem_nhds hx.2.1)
  simpa only [IsBot, not_forall, not_le] using hx.right.right.right
case H
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
z : α → α
hz : ∀ (x : α), x ∈ t → z x < x
h'z : ∀ (x : α), x ∈ t → Ioc (z x) x ⊆ a
⊢ Set.Countable {x | x ∈ {x | ∃ y, x ⋖ y} ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
case H
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
this : ∀ (x : α), x ∈ t → ∃ z, z < x ∧ Ioc z x ⊆ a
⊢ Set.Countable {x | x ∈ {x | ∃ y, x ⋖ y} ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
choose! z hz h'z using this
case H
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
z : α → α
hz : ∀ (x : α), x ∈ t → z x < x
h'z : ∀ (x : α), x ∈ t → Ioc (z x) x ⊆ a
this : PairwiseDisjoint t fun x => Ioc (z x) x
x : α
hx : x ∈ t
⊢ IsOpen (Ioc (z x) x)
case H
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
z : α → α
hz : ∀ (x : α), x ∈ t → z x < x
h'z : ∀ (x : α), x ∈ t → Ioc (z x) x ⊆ a
this : PairwiseDisjoint t fun x => Ioc (z x) x
⊢ Set.Countable {x | x ∈ {x | ∃ y, x ⋖ y} ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
refine' this.countable_of_isOpen (fun x hx => _) fun x hx => ⟨x, hz x hx, le_rfl⟩
case H
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
z : α → α
hz : ∀ (x : α), x ∈ t → z x < x
h'z : ∀ (x : α), x ∈ t → Ioc (z x) x ⊆ a
this : PairwiseDisjoint t fun x => Ioc (z x) x
x : α
hx : x ∈ t
H : Ioc (z x) x = Ioo (z x) (y x)
⊢ IsOpen (Ioc (z x) x)

case H
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
z : α → α
hz : ∀ (x : α), x ∈ t → z x < x
h'z : ∀ (x : α), x ∈ t → Ioc (z x) x ⊆ a
this : PairwiseDisjoint t fun x => Ioc (z x) x
x : α
hx : x ∈ t
⊢ Ioc (z x) x = Ioo (z x) (y x)
case H
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
z : α → α
hz : ∀ (x : α), x ∈ t → z x < x
h'z : ∀ (x : α), x ∈ t → Ioc (z x) x ⊆ a
this : PairwiseDisjoint t fun x => Ioc (z x) x
x : α
hx : x ∈ t
⊢ IsOpen (Ioc (z x) x)
suffices H : Ioc (z x) x = Ioo (z x) (y x)
no goals
case H
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
z : α → α
hz : ∀ (x : α), x ∈ t → z x < x
h'z : ∀ (x : α), x ∈ t → Ioc (z x) x ⊆ a
this : PairwiseDisjoint t fun x => Ioc (z x) x
x : α
hx : x ∈ t
⊢ Ioc (z x) x = Ioo (z x) (y x)
exact Subset.antisymm (Ioc_subset_Ioo_right (hy x hx.1).lt) fun u hu => ⟨hu.1, Hy _ _ hx.1 hu.2⟩
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
H : ∀ (a : Set α), IsOpen a → Set.Countable {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a}
this : s ⊆ ⋃ (a : Set α) (_ : a ∈ countableBasis α), {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a}
⊢ Set.Countable {x | ∃ y, x ⋖ y}
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
H : ∀ (a : Set α), IsOpen a → Set.Countable {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a}
⊢ Set.Countable {x | ∃ y, x ⋖ y}
have : s ⊆ ⋃ a ∈ countableBasis α, { x | x ∈ s ∧ x ∈ a ∧ y x ∉ a } := fun x hx => by
  rcases (isBasis_countableBasis α).exists_mem_of_ne (hy x hx).ne with ⟨a, ab, xa, ya⟩
  exact mem_iUnion₂.2 ⟨a, ab, hx, xa, ya⟩
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
H : ∀ (a : Set α), IsOpen a → Set.Countable {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a}
this : s ⊆ ⋃ (a : Set α) (_ : a ∈ countableBasis α), {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a}
⊢ Set.Countable (⋃ (a : Set α) (_ : a ∈ countableBasis α), {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a})
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
H : ∀ (a : Set α), IsOpen a → Set.Countable {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a}
this : s ⊆ ⋃ (a : Set α) (_ : a ∈ countableBasis α), {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a}
⊢ Set.Countable {x | ∃ y, x ⋖ y}
refine Set.Countable.mono this ?_
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
H : ∀ (a : Set α), IsOpen a → Set.Countable {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a}
this : s ⊆ ⋃ (a : Set α) (_ : a ∈ countableBasis α), {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a}
a : Set α
ha : a ∈ countableBasis α
⊢ IsOpen a
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
H : ∀ (a : Set α), IsOpen a → Set.Countable {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a}
this : s ⊆ ⋃ (a : Set α) (_ : a ∈ countableBasis α), {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a}
⊢ Set.Countable (⋃ (a : Set α) (_ : a ∈ countableBasis α), {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a})
refine' Countable.biUnion (countable_countableBasis α) fun a ha => H _ _
no goals
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
H : ∀ (a : Set α), IsOpen a → Set.Countable {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a}
this : s ⊆ ⋃ (a : Set α) (_ : a ∈ countableBasis α), {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a}
a : Set α
ha : a ∈ countableBasis α
⊢ IsOpen a
exact isOpen_of_mem_countableBasis ha
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
H : ∀ (a : Set α), IsOpen a → Set.Countable {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a}
x : α
hx : x ∈ s
a : Set α
ab : a ∈ countableBasis α
xa : x ∈ a
ya : ¬y x ∈ a
⊢ x ∈ ⋃ (a : Set α) (_ : a ∈ countableBasis α), {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a}
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
H : ∀ (a : Set α), IsOpen a → Set.Countable {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a}
x : α
hx : x ∈ s
⊢ x ∈ ⋃ (a : Set α) (_ : a ∈ countableBasis α), {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a}
rcases (isBasis_countableBasis α).exists_mem_of_ne (hy x hx).ne with ⟨a, ab, xa, ya⟩
no goals
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
H : ∀ (a : Set α), IsOpen a → Set.Countable {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a}
x : α
hx : x ∈ s
a : Set α
ab : a ∈ countableBasis α
xa : x ∈ a
ya : ¬y x ∈ a
⊢ x ∈ ⋃ (a : Set α) (_ : a ∈ countableBasis α), {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a}
exact mem_iUnion₂.2 ⟨a, ab, hx, xa, ya⟩
no goals
case H
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
H : Set.Countable {x | (x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a) ∧ ¬IsBot x}
⊢ Set.Countable {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a}
exact H.of_diff (subsingleton_isBot α).countable
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
x : α
hx : x ∈ t
⊢ ∃ z, z < x ∧ Ioc z x ⊆ a
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
⊢ ∀ (x : α), x ∈ t → ∃ z, z < x ∧ Ioc z x ⊆ a
intro x hx
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
x : α
hx : x ∈ t
⊢ ∃ l, l < x
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
x : α
hx : x ∈ t
⊢ ∃ z, z < x ∧ Ioc z x ⊆ a
apply exists_Ioc_subset_of_mem_nhds (ha.mem_nhds hx.2.1)
no goals
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
x : α
hx : x ∈ t
⊢ ∃ l, l < x
simpa only [IsBot, not_forall, not_le] using hx.right.right.right
case inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
z : α → α
hz : ∀ (x : α), x ∈ t → z x < x
h'z : ∀ (x : α), x ∈ t → Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x < x'
⊢ (Disjoint on fun x => Ioc (z x) x) x x'

case inr
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
z : α → α
hz : ∀ (x : α), x ∈ t → z x < x
h'z : ∀ (x : α), x ∈ t → Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x' < x
⊢ (Disjoint on fun x => Ioc (z x) x) x x'
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
z : α → α
hz : ∀ (x : α), x ∈ t → z x < x
h'z : ∀ (x : α), x ∈ t → Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
⊢ (Disjoint on fun x => Ioc (z x) x) x x'
rcases hxx'.lt_or_lt with (h' | h')
case inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
z : α → α
hz : ∀ (x : α), x ∈ t → z x < x
h'z : ∀ (x : α), x ∈ t → Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x < x'
u : α
ux : u ∈ (fun x => Ioc (z x) x) x
ux' : u ∈ (fun x => Ioc (z x) x) x'
⊢ y x ∈ a
case inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
z : α → α
hz : ∀ (x : α), x ∈ t → z x < x
h'z : ∀ (x : α), x ∈ t → Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x < x'
⊢ (Disjoint on fun x => Ioc (z x) x) x x'
refine' disjoint_left.2 fun u ux ux' => xt.2.2.1 _
case inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
z : α → α
hz : ∀ (x : α), x ∈ t → z x < x
h'z : ∀ (x : α), x ∈ t → Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x < x'
u : α
ux : u ∈ (fun x => Ioc (z x) x) x
ux' : u ∈ (fun x => Ioc (z x) x) x'
⊢ y x ≤ x'
case inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
z : α → α
hz : ∀ (x : α), x ∈ t → z x < x
h'z : ∀ (x : α), x ∈ t → Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x < x'
u : α
ux : u ∈ (fun x => Ioc (z x) x) x
ux' : u ∈ (fun x => Ioc (z x) x) x'
⊢ y x ∈ a
refine' h'z x' x't ⟨ux'.1.trans_le (ux.2.trans (hy x xt.1).le), _⟩
case inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
z : α → α
hz : ∀ (x : α), x ∈ t → z x < x
h'z : ∀ (x : α), x ∈ t → Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x < x'
u : α
ux : u ∈ (fun x => Ioc (z x) x) x
ux' : u ∈ (fun x => Ioc (z x) x) x'
H : x' < y x
⊢ False
case inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
z : α → α
hz : ∀ (x : α), x ∈ t → z x < x
h'z : ∀ (x : α), x ∈ t → Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x < x'
u : α
ux : u ∈ (fun x => Ioc (z x) x) x
ux' : u ∈ (fun x => Ioc (z x) x) x'
⊢ y x ≤ x'
by_contra' H
no goals
case inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
z : α → α
hz : ∀ (x : α), x ∈ t → z x < x
h'z : ∀ (x : α), x ∈ t → Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x < x'
u : α
ux : u ∈ (fun x => Ioc (z x) x) x
ux' : u ∈ (fun x => Ioc (z x) x) x'
H : x' < y x
⊢ False
exact False.elim (lt_irrefl _ ((Hy _ _ xt.1 H).trans_lt h'))
case inr
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
z : α → α
hz : ∀ (x : α), x ∈ t → z x < x
h'z : ∀ (x : α), x ∈ t → Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x' < x
u : α
ux : u ∈ (fun x => Ioc (z x) x) x
ux' : u ∈ (fun x => Ioc (z x) x) x'
⊢ y x' ∈ a
case inr
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
z : α → α
hz : ∀ (x : α), x ∈ t → z x < x
h'z : ∀ (x : α), x ∈ t → Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x' < x
⊢ (Disjoint on fun x => Ioc (z x) x) x x'
refine' disjoint_left.2 fun u ux ux' => x't.2.2.1 _
case inr
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
z : α → α
hz : ∀ (x : α), x ∈ t → z x < x
h'z : ∀ (x : α), x ∈ t → Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x' < x
u : α
ux : u ∈ (fun x => Ioc (z x) x) x
ux' : u ∈ (fun x => Ioc (z x) x) x'
⊢ y x' ≤ x
case inr
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
z : α → α
hz : ∀ (x : α), x ∈ t → z x < x
h'z : ∀ (x : α), x ∈ t → Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x' < x
u : α
ux : u ∈ (fun x => Ioc (z x) x) x
ux' : u ∈ (fun x => Ioc (z x) x) x'
⊢ y x' ∈ a
refine' h'z x xt ⟨ux.1.trans_le (ux'.2.trans (hy x' x't.1).le), _⟩
case inr
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
z : α → α
hz : ∀ (x : α), x ∈ t → z x < x
h'z : ∀ (x : α), x ∈ t → Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x' < x
u : α
ux : u ∈ (fun x => Ioc (z x) x) x
ux' : u ∈ (fun x => Ioc (z x) x) x'
H : x < y x'
⊢ False
case inr
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
z : α → α
hz : ∀ (x : α), x ∈ t → z x < x
h'z : ∀ (x : α), x ∈ t → Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x' < x
u : α
ux : u ∈ (fun x => Ioc (z x) x) x
ux' : u ∈ (fun x => Ioc (z x) x) x'
⊢ y x' ≤ x
by_contra' H
no goals
case inr
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
z : α → α
hz : ∀ (x : α), x ∈ t → z x < x
h'z : ∀ (x : α), x ∈ t → Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x' < x
u : α
ux : u ∈ (fun x => Ioc (z x) x) x
ux' : u ∈ (fun x => Ioc (z x) x) x'
H : x < y x'
⊢ False
exact False.elim (lt_irrefl _ ((Hy _ _ x't.1 H).trans_lt h'))
case H
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
z : α → α
hz : ∀ (x : α), x ∈ t → z x < x
h'z : ∀ (x : α), x ∈ t → Ioc (z x) x ⊆ a
this : PairwiseDisjoint t fun x => Ioc (z x) x
x : α
hx : x ∈ t
H : Ioc (z x) x = Ioo (z x) (y x)
⊢ IsOpen (Ioo (z x) (y x))
case H
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
z : α → α
hz : ∀ (x : α), x ∈ t → z x < x
h'z : ∀ (x : α), x ∈ t → Ioc (z x) x ⊆ a
this : PairwiseDisjoint t fun x => Ioc (z x) x
x : α
hx : x ∈ t
H : Ioc (z x) x = Ioo (z x) (y x)
⊢ IsOpen (Ioc (z x) x)
rw [H]
no goals
case H
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ (x : α), x ∈ s → x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ ¬y x ∈ a ∧ ¬IsBot x}
z : α → α
hz : ∀ (x : α), x ∈ t → z x < x
h'z : ∀ (x : α), x ∈ t → Ioc (z x) x ⊆ a
this : PairwiseDisjoint t fun x => Ioc (z x) x
x : α
hx : x ∈ t
H : Ioc (z x) x = Ioo (z x) (y x)
⊢ IsOpen (Ioo (z x) (y x))
exact isOpen_Ioo