internlm/Lean-Github huggingface dataset:
Theorem: infi₂_le_iff
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
f : α → β
s : Set α
b : β
⊢ ⨅ x ∈ s, f x ≤ b ↔ ∀ (b' : β), (∀ x ∈ s, b' ≤ f x) → b' ≤ b
Tactic:
rw [iInf_le_iff]
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
f : α → β
s : Set α
b : β
⊢ (∀ (b_1 : β), (∀ (i : α), b_1 ≤ ⨅ (_ : i ∈ s), f i) → b_1 ≤ b) ↔ ∀ (b' : β), (∀ x ∈ s, b' ≤ f x) → b' ≤ b
Theorem: infi₂_le_iff
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
f : α → β
s : Set α
b : β
⊢ (∀ (b_1 : β), (∀ (i : α), b_1 ≤ ⨅ (_ : i ∈ s), f i) → b_1 ≤ b) ↔ ∀ (b' : β), (∀ x ∈ s, b' ≤ f x) → b' ≤ b
Tactic:
apply forall_congr'
Proof state after:
case h
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
f : α → β
s : Set α
b : β
⊢ ∀ (a : β), (∀ (i : α), a ≤ ⨅ (_ : i ∈ s), f i) → a ≤ b ↔ (∀ x ∈ s, a ≤ f x) → a ≤ b
Theorem: infi₂_le_iff
Proof state before:
case h
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
f : α → β
s : Set α
b : β
⊢ ∀ (a : β), (∀ (i : α), a ≤ ⨅ (_ : i ∈ s), f i) → a ≤ b ↔ (∀ x ∈ s, a ≤ f x) → a ≤ b
Tactic:
intro b'
Proof state after:
case h
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
f : α → β
s : Set α
b b' : β
⊢ (∀ (i : α), b' ≤ ⨅ (_ : i ∈ s), f i) → b' ≤ b ↔ (∀ x ∈ s, b' ≤ f x) → b' ≤ b
Theorem: infi₂_le_iff
Proof state before:
case h
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
f : α → β
s : Set α
b b' : β
⊢ (∀ (i : α), b' ≤ ⨅ (_ : i ∈ s), f i) → b' ≤ b ↔ (∀ x ∈ s, b' ≤ f x) → b' ≤ b
Tactic:
simp_rw [le_iInf_iff]
Proof state after:
no goals
Theorem: IsPreconnected.subset_or_subset_of_closed
Proof state before:
α : Type u_1
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : IsPreconnected s
⊢ s ⊆ u ∨ s ⊆ v
Tactic:
apply (isPreconnected_iff_subset_of_disjoint_closed.mp hs) u v hu hv hsuv
Proof state after:
α : Type u_1
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : IsPreconnected s
⊢ s ∩ (u ∩ v) = ∅
Theorem: IsPreconnected.subset_or_subset_of_closed
Proof state before:
α : Type u_1
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : IsPreconnected s
⊢ s ∩ (u ∩ v) = ∅
Tactic:
rw [Set.disjoint_iff_inter_eq_empty.mp huv, Set.inter_empty]
Proof state after:
no goals
Theorem: Filter.frequently_congr
Proof state before:
α : Type u_1
f : Filter α
p q : α → Prop
h : ∀ᶠ (x : α) in f, p x ↔ q x
hq : ∃ᶠ (x : α) in f, q x
⊢ ∀ᶠ (x : α) in f, q x ↔ p x
Tactic:
simpa only [Iff.comm] using h
Proof state after:
no goals
Theorem: Filter.frequently_congr'
Proof state before:
α✝ : Type ?u.1842
α : Type u_1
f : Filter α
p q : α → Prop
h : ∀ᶠ (a : α) in f, p a ↔ q a
⊢ (∃ᶠ (a : α) in f, p a) ↔ ∃ᶠ (a : α) in f, q a
Tactic:
dsimp only [Filter.Frequently]
Proof state after:
α✝ : Type ?u.1842
α : Type u_1
f : Filter α
p q : α → Prop
h : ∀ᶠ (a : α) in f, p a ↔ q a
⊢ (¬∀ᶠ (x : α) in f, ¬p x) ↔ ¬∀ᶠ (x : α) in f, ¬q x
Theorem: Filter.frequently_congr'
Proof state before:
α✝ : Type ?u.1842
α : Type u_1
f : Filter α
p q : α → Prop
h : ∀ᶠ (a : α) in f, p a ↔ q a
⊢ (¬∀ᶠ (x : α) in f, ¬p x) ↔ ¬∀ᶠ (x : α) in f, ¬q x
Tactic:
rw [not_iff_not]
Proof state after:
α✝ : Type ?u.1842
α : Type u_1
f : Filter α
p q : α → Prop
h : ∀ᶠ (a : α) in f, p a ↔ q a
⊢ (∀ᶠ (x : α) in f, ¬p x) ↔ ∀ᶠ (x : α) in f, ¬q x
Theorem: Filter.frequently_congr'
Proof state before:
α✝ : Type ?u.1842
α : Type u_1
f : Filter α
p q : α → Prop
h : ∀ᶠ (a : α) in f, p a ↔ q a
⊢ (∀ᶠ (x : α) in f, ¬p x) ↔ ∀ᶠ (x : α) in f, ¬q x
Tactic:
apply Filter.eventually_congr
Proof state after:
case h
α✝ : Type ?u.1842
α : Type u_1
f : Filter α
p q : α → Prop
h : ∀ᶠ (a : α) in f, p a ↔ q a
⊢ ∀ᶠ (x : α) in f, ¬p x ↔ ¬q x
Theorem: Filter.frequently_congr'
Proof state before:
case h
α✝ : Type ?u.1842
α : Type u_1
f : Filter α
p q : α → Prop
h : ∀ᶠ (a : α) in f, p a ↔ q a
⊢ ∀ᶠ (x : α) in f, ¬p x ↔ ¬q x
Tactic:
simp_rw [not_iff_not]
Proof state after:
case h
α✝ : Type ?u.1842
α : Type u_1
f : Filter α
p q : α → Prop
h : ∀ᶠ (a : α) in f, p a ↔ q a
⊢ ∀ᶠ (x : α) in f, p x ↔ q x
Theorem: Filter.frequently_congr'
Proof state before:
case h
α✝ : Type ?u.1842
α : Type u_1
f : Filter α
p q : α → Prop
h : ∀ᶠ (a : α) in f, p a ↔ q a
⊢ ∀ᶠ (x : α) in f, p x ↔ q x
Tactic:
exact h
Proof state after:
no goals
Theorem: Filter.clusterPt_principal_subtype_iff_frequently
Proof state before:
α✝ : Type ?u.2106
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ ClusterPt a (𝓟 J) ↔ ∃ᶠ (x : α) in nhdsWithin (↑a) t, ∃ (h : x ∈ s), { val := x, property := h } ∈ J
Tactic:
rw [nhdsWithin_eq_map_subtype_coe (hst a.prop), Filter.frequently_map,
  clusterPt_principal_iff_frequently, inducing_subtype_val.nhds_eq_comap, Filter.frequently_comap,
  inducing_subtype_val.nhds_eq_comap, Filter.frequently_comap, Subtype.coe_mk]
Proof state after:
α✝ : Type ?u.2106
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ (∃ᶠ (b : α) in nhds ↑a, ∃ a, ↑a = b ∧ a ∈ J) ↔
    ∃ᶠ (b : α) in nhds ↑a, ∃ a, ↑a = b ∧ ∃ (h : ↑a ∈ s), { val := ↑a, property := h } ∈ J
Theorem: Filter.clusterPt_principal_subtype_iff_frequently
Proof state before:
α✝ : Type ?u.2106
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ (∃ᶠ (b : α) in nhds ↑a, ∃ a, ↑a = b ∧ a ∈ J) ↔
    ∃ᶠ (b : α) in nhds ↑a, ∃ a, ↑a = b ∧ ∃ (h : ↑a ∈ s), { val := ↑a, property := h } ∈ J
Tactic:
apply frequently_congr
Proof state after:
case h
α✝ : Type ?u.2106
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ ∀ᶠ (x : α) in nhds ↑a, (∃ a, ↑a = x ∧ a ∈ J) ↔ ∃ a, ↑a = x ∧ ∃ (h : ↑a ∈ s), { val := ↑a, property := h } ∈ J
Theorem: Filter.clusterPt_principal_subtype_iff_frequently
Proof state before:
case h
α✝ : Type ?u.2106
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ ∀ᶠ (x : α) in nhds ↑a, (∃ a, ↑a = x ∧ a ∈ J) ↔ ∃ a, ↑a = x ∧ ∃ (h : ↑a ∈ s), { val := ↑a, property := h } ∈ J
Tactic:
apply eventually_of_forall
Proof state after:
case h.hp
α✝ : Type ?u.2106
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ ∀ (x : α), (∃ a, ↑a = x ∧ a ∈ J) ↔ ∃ a, ↑a = x ∧ ∃ (h : ↑a ∈ s), { val := ↑a, property := h } ∈ J
Theorem: Filter.clusterPt_principal_subtype_iff_frequently
Proof state before:
case h.hp
α✝ : Type ?u.2106
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ ∀ (x : α), (∃ a, ↑a = x ∧ a ∈ J) ↔ ∃ a, ↑a = x ∧ ∃ (h : ↑a ∈ s), { val := ↑a, property := h } ∈ J
Tactic:
intro x
Proof state after:
case h.hp
α✝ : Type ?u.2106
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
x : α
⊢ (∃ a, ↑a = x ∧ a ∈ J) ↔ ∃ a, ↑a = x ∧ ∃ (h : ↑a ∈ s), { val := ↑a, property := h } ∈ J
Theorem: Filter.clusterPt_principal_subtype_iff_frequently
Proof state before:
case h.hp
α✝ : Type ?u.2106
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
x : α
⊢ (∃ a, ↑a = x ∧ a ∈ J) ↔ ∃ a, ↑a = x ∧ ∃ (h : ↑a ∈ s), { val := ↑a, property := h } ∈ J
Tactic:
simp only [Subtype.coe_mk, SetCoe.exists, exists_and_left, exists_eq_left]
Proof state after:
case h.hp
α✝ : Type ?u.2106
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
x : α
⊢ (∃ (x_1 : x ∈ s), { val := x, property := ⋯ } ∈ J) ↔ ∃ (x_1 : x ∈ t) (h : x ∈ s), { val := x, property := ⋯ } ∈ J
Theorem: Filter.clusterPt_principal_subtype_iff_frequently
Proof state before:
case h.hp
α✝ : Type ?u.2106
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
x : α
⊢ (∃ (x_1 : x ∈ s), { val := x, property := ⋯ } ∈ J) ↔ ∃ (x_1 : x ∈ t) (h : x ∈ s), { val := x, property := ⋯ } ∈ J
Tactic:
exact ⟨fun ⟨h, hx⟩ => ⟨hst h, h, hx⟩, fun ⟨_, hx⟩ => hx⟩
Proof state after:
no goals
Theorem: min_mem_of_mem
Proof state before:
α✝ : Type ?u.5660
α : Type u_1
inst✝ : LinearOrder α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
⊢ min a b ∈ s
Tactic:
rw [min_def]
Proof state after:
α✝ : Type ?u.5660
α : Type u_1
inst✝ : LinearOrder α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
⊢ (if a ≤ b then a else b) ∈ s
Theorem: min_mem_of_mem
Proof state before:
α✝ : Type ?u.5660
α : Type u_1
inst✝ : LinearOrder α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
⊢ (if a ≤ b then a else b) ∈ s
Tactic:
split_ifs <;> assumption
Proof state after:
no goals
Theorem: max_mem_of_mem
Proof state before:
α✝ : Type ?u.6414
α : Type u_1
inst✝ : LinearOrder α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
⊢ max a b ∈ s
Tactic:
rw [max_def]
Proof state after:
α✝ : Type ?u.6414
α : Type u_1
inst✝ : LinearOrder α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
⊢ (if a ≤ b then b else a) ∈ s
Theorem: max_mem_of_mem
Proof state before:
α✝ : Type ?u.6414
α : Type u_1
inst✝ : LinearOrder α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
⊢ (if a ≤ b then b else a) ∈ s
Tactic:
split_ifs <;> assumption
Proof state after:
no goals
Theorem: inf_mem_of_mem
Proof state before:
α✝ : Type ?u.7108
α : Type u_1
inst✝ : LinearOrder α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
⊢ a ⊓ b ∈ s
Tactic:
rw [inf_eq_min]
Proof state after:
α✝ : Type ?u.7108
α : Type u_1
inst✝ : LinearOrder α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
⊢ min a b ∈ s
Theorem: inf_mem_of_mem
Proof state before:
α✝ : Type ?u.7108
α : Type u_1
inst✝ : LinearOrder α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
⊢ min a b ∈ s
Tactic:
exact min_mem_of_mem ha hb
Proof state after:
no goals
Theorem: sup_mem_of_mem
Proof state before:
α✝ : Type ?u.7628
α : Type u_1
inst✝ : LinearOrder α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
⊢ a ⊔ b ∈ s
Tactic:
rw [sup_eq_max]
Proof state after:
α✝ : Type ?u.7628
α : Type u_1
inst✝ : LinearOrder α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
⊢ max a b ∈ s
Theorem: sup_mem_of_mem
Proof state before:
α✝ : Type ?u.7628
α : Type u_1
inst✝ : LinearOrder α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
⊢ max a b ∈ s
Tactic:
exact max_mem_of_mem ha hb
Proof state after:
no goals
Theorem: IsTotal.directed'
Proof state before:
α : Type u_1
ι : Sort u_2
r : α → α → Prop
inst✝ : IsTotal α r
f : ι → α
i j : ι
⊢ ∃ z, r (f i) (f z) ∧ r (f j) (f z)
Tactic:
cases (total_of r (f i) (f j)) with
| inl h => exact ⟨j, h, refl _⟩
| inr h => exact ⟨i, refl _, h⟩
Proof state after:
no goals
Theorem: IsTotal.directed'
Proof state before:
case inl
α : Type u_1
ι : Sort u_2
r : α → α → Prop
inst✝ : IsTotal α r
f : ι → α
i j : ι
h : r (f i) (f j)
⊢ ∃ z, r (f i) (f z) ∧ r (f j) (f z)
Tactic:
exact ⟨j, h, refl _⟩
Proof state after:
no goals
Theorem: IsTotal.directed'
Proof state before:
case inr
α : Type u_1
ι : Sort u_2
r : α → α → Prop
inst✝ : IsTotal α r
f : ι → α
i j : ι
h : r (f j) (f i)
⊢ ∃ z, r (f i) (f z) ∧ r (f j) (f z)
Tactic:
exact ⟨i, refl _, h⟩
Proof state after:
no goals
Theorem: LowerSemicontinuousWithinAt.sup
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
⊢ LowerSemicontinuousWithinAt (fun x => f x ⊔ g x) s a
Tactic:
intro b hb
Proof state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < (fun x => f x ⊔ g x) a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < (fun x => f x ⊔ g x) x'
Theorem: LowerSemicontinuousWithinAt.sup
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < (fun x => f x ⊔ g x) a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < (fun x => f x ⊔ g x) x'
Tactic:
simp only [lt_sup_iff] at hb ⊢
Proof state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < f a ∨ b < g a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'
Theorem: LowerSemicontinuousWithinAt.sup
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < f a ∨ b < g a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'
Tactic:
cases' hb with hb hb
Proof state after:
case inl
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < f a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'

case inr
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < g a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'
Theorem: LowerSemicontinuousWithinAt.sup
Proof state before:
case inl
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < f a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'
Tactic:
filter_upwards [hf b hb] with x using Or.intro_left _
Proof state after:
no goals
Theorem: LowerSemicontinuousWithinAt.sup
Proof state before:
case inr
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < g a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'
Tactic:
filter_upwards [hg b hb] with x using Or.intro_right _
Proof state after:
no goals
Theorem: LowerSemicontinuousAt.sup
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
a : α
hf : LowerSemicontinuousAt f a
hg : LowerSemicontinuousAt g a
⊢ LowerSemicontinuousAt (fun x => f x ⊔ g x) a
Tactic:
rw [← lowerSemicontinuousWithinAt_univ_iff] at *
Proof state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
a : α
hf : LowerSemicontinuousWithinAt f univ a
hg : LowerSemicontinuousWithinAt g univ a
⊢ LowerSemicontinuousWithinAt (fun x => f x ⊔ g x) univ a
Theorem: LowerSemicontinuousAt.sup
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
a : α
hf : LowerSemicontinuousWithinAt f univ a
hg : LowerSemicontinuousWithinAt g univ a
⊢ LowerSemicontinuousWithinAt (fun x => f x ⊔ g x) univ a
Tactic:
exact hf.sup hg
Proof state after:
no goals
Theorem: LowerSemicontinuousWithinAt.inf
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
⊢ LowerSemicontinuousWithinAt (fun x => f x ⊓ g x) s a
Tactic:
intro b hb
Proof state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < (fun x => f x ⊓ g x) a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < (fun x => f x ⊓ g x) x'
Theorem: LowerSemicontinuousWithinAt.inf
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < (fun x => f x ⊓ g x) a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < (fun x => f x ⊓ g x) x'
Tactic:
simp only [lt_inf_iff] at hb ⊢
Proof state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < f a ∧ b < g a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∧ b < g x'
Theorem: LowerSemicontinuousWithinAt.inf
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < f a ∧ b < g a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∧ b < g x'
Tactic:
exact Eventually.and (hf b hb.1) (hg b hb.2)
Proof state after:
no goals
Theorem: LowerSemicontinuousAt.inf
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
a : α
hf : LowerSemicontinuousAt f a
hg : LowerSemicontinuousAt g a
⊢ LowerSemicontinuousAt (fun x => f x ⊓ g x) a
Tactic:
rw [← lowerSemicontinuousWithinAt_univ_iff] at *
Proof state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
a : α
hf : LowerSemicontinuousWithinAt f univ a
hg : LowerSemicontinuousWithinAt g univ a
⊢ LowerSemicontinuousWithinAt (fun x => f x ⊓ g x) univ a
Theorem: LowerSemicontinuousAt.inf
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
g : α → β
a : α
hf : LowerSemicontinuousWithinAt f univ a
hg : LowerSemicontinuousWithinAt g univ a
⊢ LowerSemicontinuousWithinAt (fun x => f x ⊓ g x) univ a
Tactic:
exact hf.inf hg
Proof state after:
no goals
Theorem: lowerSemicontinuousOn_iff_restrict
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
⊢ LowerSemicontinuousOn f s ↔ LowerSemicontinuous (restrict s f)
Tactic:
rw [LowerSemicontinuousOn, LowerSemicontinuous, SetCoe.forall]
Proof state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
⊢ (∀ x ∈ s, LowerSemicontinuousWithinAt f s x) ↔
    ∀ (x : α) (h : x ∈ s), LowerSemicontinuousAt (restrict s f) { val := x, property := h }
Theorem: lowerSemicontinuousOn_iff_restrict
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
⊢ (∀ x ∈ s, LowerSemicontinuousWithinAt f s x) ↔
    ∀ (x : α) (h : x ∈ s), LowerSemicontinuousAt (restrict s f) { val := x, property := h }
Tactic:
refine' forall₂_congr fun a ha => forall₂_congr fun b _ => _
Proof state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
a : α
ha : a ∈ s
b : β
x✝ : b < f a
⊢ (∀ᶠ (x' : α) in 𝓝[s] a, b < f x') ↔ ∀ᶠ (x' : ↑s) in 𝓝 { val := a, property := ha }, b < restrict s f x'
Theorem: lowerSemicontinuousOn_iff_restrict
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
a : α
ha : a ∈ s
b : β
x✝ : b < f a
⊢ (∀ᶠ (x' : α) in 𝓝[s] a, b < f x') ↔ ∀ᶠ (x' : ↑s) in 𝓝 { val := a, property := ha }, b < restrict s f x'
Tactic:
simp only [nhdsWithin_eq_map_subtype_coe ha, eventually_map, restrict]
Proof state after:
no goals
Theorem: lowerSemicontinuousOn_iff_preimage_Ioi
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
⊢ LowerSemicontinuousOn f s ↔ ∀ (b : β), ∃ u, IsOpen u ∧ s ∩ f ⁻¹' Ioi b = s ∩ u
Tactic:
simp only [lowerSemicontinuousOn_iff_restrict, restrict_eq,
  lowerSemicontinuous_iff_isOpen_preimage, preimage_comp, isOpen_induced_iff,
  Subtype.preimage_coe_eq_preimage_coe_iff, eq_comm]
Proof state after:
no goals
Theorem: lowerSemicontinuousOn_iff_preimage_Iic
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
⊢ LowerSemicontinuousOn f s ↔ ∀ (b : β), ∃ v, IsClosed v ∧ s ∩ f ⁻¹' Iic b = s ∩ v
Tactic:
simp only [lowerSemicontinuousOn_iff_restrict, restrict_eq,
  lowerSemicontinuous_iff_isClosed_preimage, preimage_comp, isClosed_induced_iff,
  Subtype.preimage_coe_eq_preimage_coe_iff, eq_comm]
Proof state after:
no goals
Theorem: LowerSemicontinuousOn.exists_forall_le_of_isCompact
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
Tactic:
haveI : Nonempty α := ⟨ne_s.choose⟩
Proof state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this : Nonempty α
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
Theorem: LowerSemicontinuousOn.exists_forall_le_of_isCompact
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this : Nonempty α
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
Tactic:
haveI : Nonempty s := ⟨⟨ne_s.choose, ne_s.choose_spec⟩⟩
Proof state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝ : Nonempty α
this : Nonempty ↑s
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
Theorem: LowerSemicontinuousOn.exists_forall_le_of_isCompact
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝ : Nonempty α
this : Nonempty ↑s
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
Tactic:
let φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
Proof state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝ : Nonempty α
this : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
Theorem: LowerSemicontinuousOn.exists_forall_le_of_isCompact
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝ : Nonempty α
this : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
Tactic:
let ℱ : Filter α := ⨅ a : s, φ (f a)
Proof state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝ : Nonempty α
this : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x