awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
ι : Type u_4
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt (β := ℝ≥0∞) (fun (x' : α) ↦ ∑' (i : ι), f i x') univ x

Tactic:
lowerSemicontinuousWithinAt_tsum h

Premises used: lowerSemicontinuousWithinAt_tsum
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
ι : Type u_4
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt (β := ℝ≥0∞) (fun (x' : α) ↦ ∑' (i : ι), f i x') univ x

Tactic:
exact lowerSemicontinuousWithinAt_tsum h

Premises used: lowerSemicontinuousWithinAt_tsum
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
ι : Type u_4
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousOn (f i) s
⊢ LowerSemicontinuousOn (β := ℝ≥0∞) (fun (x' : α) ↦ ∑' (i : ι), f i x') s

Tactic:
fun x hx =>
  lowerSemicontinuousWithinAt_tsum fun i => h i x hx

Premises used: lowerSemicontinuousWithinAt_tsum, SemicontinuousOn
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_4
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuous (f i)
⊢ LowerSemicontinuous (β := ℝ≥0∞) fun (x' : α) ↦ ∑' (i : ι), f i x'

Tactic:
fun x => lowerSemicontinuousAt_tsum fun i => h i x

Premises used: lowerSemicontinuousAt_tsum, Semicontinuous
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
inst : TopologicalSpace α
β : Type u_5
inst_1 : LinearOrder β
f : α → β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : UpperSemicontinuousOn f s
⊢ ∃ a ∈ s, IsMaxOn f s a

Tactic:
LowerSemicontinuousOn.exists_isMinOn (β := βᵒᵈ) ne_s hs hf

Premises used: IsMaxOn, LowerSemicontinuousOn.exists_isMinOn, IsMaxFilter
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
inst : TopologicalSpace α
β : Type u_5
inst_1 : LinearOrder β
f : α → β
inst_2 : Nonempty β
s : Set α
hs : IsCompact s
hf : UpperSemicontinuousOn f s
⊢ BddAbove (f '' s)

Tactic:
LowerSemicontinuousOn.bddBelow_of_isCompact (β := βᵒᵈ) hs hf

Premises used: Set.Mem, setOf, upperBounds, LowerSemicontinuousOn.bddBelow_of_isCompact, BddAbove, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsOpen[inst] s
hy : y ≤ 0
⊢ UpperSemicontinuous.{u_1, u_2} (β := β) (s.indicator fun (_x : α) ↦ y)

Tactic:
IsOpen.lowerSemicontinuous_indicator (β := βᵒᵈ) hs hy

Premises used: IsOpen.lowerSemicontinuous_indicator, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s t : Set α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsOpen[inst] s
hy : y ≤ 0
⊢ UpperSemicontinuousOn.{u_1, u_2} (β := β) (s.indicator fun (_x : α) ↦ y) t

Tactic:
(hs.upperSemicontinuous_indicator hy).upperSemicontinuousOn t

Premises used: IsOpen.upperSemicontinuous_indicator, UpperSemicontinuous.upperSemicontinuousOn
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
x : α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsOpen[inst] s
hy : y ≤ 0
⊢ UpperSemicontinuousAt.{u_1, u_2} (β := β) (s.indicator fun (_x : α) ↦ y) x

Tactic:
(hs.upperSemicontinuous_indicator hy).upperSemicontinuousAt x

Premises used: IsOpen.upperSemicontinuous_indicator, UpperSemicontinuous.upperSemicontinuousAt
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s t : Set α
x : α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsOpen[inst] s
hy : y ≤ 0
⊢ UpperSemicontinuousWithinAt.{u_1, u_2} (β := β) (s.indicator fun (_x : α) ↦ y) t x

Tactic:
(hs.upperSemicontinuous_indicator hy).upperSemicontinuousWithinAt t x

Premises used: UpperSemicontinuous.upperSemicontinuousWithinAt, IsOpen.upperSemicontinuous_indicator
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsClosed[inst] s
hy : 0 ≤ y
⊢ UpperSemicontinuous.{u_1, u_2} (β := β) (s.indicator fun (_x : α) ↦ y)

Tactic:
IsClosed.lowerSemicontinuous_indicator (β := βᵒᵈ) hs hy

Premises used: IsClosed.lowerSemicontinuous_indicator, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s t : Set α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsClosed[inst] s
hy : 0 ≤ y
⊢ UpperSemicontinuousOn.{u_1, u_2} (β := β) (s.indicator fun (_x : α) ↦ y) t

Tactic:
(hs.upperSemicontinuous_indicator hy).upperSemicontinuousOn t

Premises used: IsClosed.upperSemicontinuous_indicator, UpperSemicontinuous.upperSemicontinuousOn
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
x : α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsClosed[inst] s
hy : 0 ≤ y
⊢ UpperSemicontinuousAt.{u_1, u_2} (β := β) (s.indicator fun (_x : α) ↦ y) x

Tactic:
(hs.upperSemicontinuous_indicator hy).upperSemicontinuousAt x

Premises used: IsClosed.upperSemicontinuous_indicator, UpperSemicontinuous.upperSemicontinuousAt
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s t : Set α
x : α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsClosed[inst] s
hy : 0 ≤ y
⊢ UpperSemicontinuousWithinAt.{u_1, u_2} (β := β) (s.indicator fun (_x : α) ↦ y) t x

Tactic:
(hs.upperSemicontinuous_indicator hy).upperSemicontinuousWithinAt t x

Premises used: UpperSemicontinuous.upperSemicontinuousWithinAt, IsClosed.upperSemicontinuous_indicator
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : Preorder β
⊢ UpperSemicontinuous f ↔ ∀ (y : β), IsOpen[inst] (f ⁻¹' Iio y)

Tactic:
⟨fun H y => isOpen_iff_mem_nhds.2 fun x hx => H x y hx, fun H _x y y_lt =>
    IsOpen.mem_nhds (H y) y_lt⟩

Premises used: Iff.mpr, IsOpen.mem_nhds, Iff.intro, isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : Preorder β
hf : UpperSemicontinuous f
y : β
⊢ IsOpen[inst] (f ⁻¹' Iio y)

Tactic:
upperSemicontinuous_iff_isOpen_preimage.1 hf y

Premises used: Iff.mp, upperSemicontinuous_iff_isOpen_preimage
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
f : α → γ
rw : (∀ (y : γ), IsOpen[inst] (f ⁻¹' Iio y)) ↔ ∀ (y : γ), IsClosed[inst] (f ⁻¹' Ici y)
⊢ UpperSemicontinuous f ↔ ∀ (y : γ), IsClosed[inst] (f ⁻¹' Ici y)

Tactic:
rw [upperSemicontinuous_iff_isOpen_preimage]

Premises used: upperSemicontinuous_iff_isOpen_preimage
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
f : α → γ
⊢ (∀ (y : γ), IsOpen[inst] (f ⁻¹' Iio y)) ↔ ∀ (y : γ), IsClosed[inst] (f ⁻¹' Ici y)

Tactic:
simp only [← isOpen_compl_iff, ← preimage_compl, compl_Ici]

Premises used: Set.compl_Ici, Set.preimage_compl, isOpen_compl_iff
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
f : α → γ
hf : UpperSemicontinuous f
y : γ
⊢ IsClosed[inst] (f ⁻¹' Ici y)

Tactic:
upperSemicontinuous_iff_isClosed_preimage.1 hf y

Premises used: upperSemicontinuous_iff_isClosed_preimage, Iff.mp
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
f : α → γ
h : ContinuousWithinAt f s x
⊢ UpperSemicontinuousWithinAt f s x

Tactic:
fun _y hy => h (Iio_mem_nhds hy)

Premises used: Iio_mem_nhds, Set.Mem, Filter.Eventually, setOf, Set.preimage, Set.Iio, SemicontinuousWithinAt
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
f : α → γ
h : ContinuousAt f x
⊢ UpperSemicontinuousAt f x

Tactic:
fun _y hy => h (Iio_mem_nhds hy)

Premises used: Iio_mem_nhds, Set.Mem, Filter.Eventually, setOf, Set.preimage, Set.Iio, SemicontinuousAt
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
f : α → γ
h : ContinuousOn f s
⊢ UpperSemicontinuousOn f s

Tactic:
fun x hx => (h x hx).upperSemicontinuousWithinAt

Premises used: SemicontinuousOn, ContinuousWithinAt.upperSemicontinuousWithinAt
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
f : α → γ
h : Continuous[inst, inst_2] f
⊢ UpperSemicontinuous f

Tactic:
fun _x => h.continuousAt.upperSemicontinuousAt

Premises used: Continuous.continuousAt, Semicontinuous, ContinuousAt.upperSemicontinuousAt
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : CompleteLinearOrder γ
f : α → γ
⊢ UpperSemicontinuousWithinAt f s x ↔ limsup f (𝓝[s] x) ≤ f x

Tactic:
lowerSemicontinuousWithinAt_iff_le_liminf (γ := γᵒᵈ)

Premises used: Filter.limsSup, setOf, Filter.limsup, lowerSemicontinuousWithinAt_iff_le_liminf, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
γ : Type u_4
inst_1 : CompleteLinearOrder γ
f : α → γ
⊢ UpperSemicontinuousAt f x ↔ limsup f (𝓝 x) ≤ f x

Tactic:
lowerSemicontinuousAt_iff_le_liminf (γ := γᵒᵈ)

Premises used: Filter.limsSup, setOf, Filter.limsup, lowerSemicontinuousAt_iff_le_liminf, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : CompleteLinearOrder γ
f : α → γ
⊢ UpperSemicontinuous f ↔ ∀ (x : α), limsup f (𝓝 x) ≤ f x

Tactic:
lowerSemicontinuous_iff_le_liminf (γ := γᵒᵈ)

Premises used: Filter.limsSup, lowerSemicontinuous_iff_le_liminf, setOf, Filter.limsup, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : CompleteLinearOrder γ
f : α → γ
⊢ UpperSemicontinuousOn f s ↔ ∀ x ∈ s, limsup f (𝓝[s] x) ≤ f x

Tactic:
lowerSemicontinuousOn_iff_le_liminf (γ := γᵒᵈ)

Premises used: Filter.limsSup, setOf, Filter.limsup, OrderDual, lowerSemicontinuousOn_iff_le_liminf
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : LinearOrder γ
f : α → γ
hfs : UpperSemicontinuousOn f s
ks : IsCompact s
c : γ
⊢ IsCompact (s ∩ f ⁻¹' Ici c)

Tactic:
LowerSemicontinuousOn.isCompact_inter_preimage_Iic (γ := γᵒᵈ) hfs ks c

Premises used: Set.Ici, setOf, LowerSemicontinuousOn.isCompact_inter_preimage_Iic, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, UpperSemicontinuousOn (f i) s
⊢ s ∩ ⋂ i ∈ I, f i ⁻¹' Ici c = ∅ ↔ ∃ (u : Finset (↑I : Type u_5)), ∀ x ∈ s, ∃ i ∈ u, f (↑i : ι) x < c

Tactic:
LowerSemicontinuousOn.inter_biInter_preimage_Iic_eq_empty_iff_exists_finset ks hfi (γ := γᵒᵈ)

Premises used: LowerSemicontinuousOn.inter_biInter_preimage_Iic_eq_empty_iff_exists_finset, Set.Ici, setOf, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : ClosedIicTopology γ
f : α → γ
hs : IsClosed[inst] s
⊢ UpperSemicontinuousOn f s ↔ IsClosed[instTopologicalSpaceProd] {p : α × γ | p.1 ∈ s ∧ p.2 ≤ f p.1}

Tactic:
lowerSemicontinuousOn_iff_isClosed_epigraph hs (γ := γᵒᵈ)

Premises used: Set.Mem, setOf, lowerSemicontinuousOn_iff_isClosed_epigraph, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : ClosedIicTopology γ
f : α → γ
⊢ UpperSemicontinuous f ↔ IsClosed[instTopologicalSpaceProd] {p : α × γ | p.2 ≤ f p.1}

Tactic:
lowerSemicontinuous_iff_isClosed_epigraph (γ := γᵒᵈ)

Premises used: setOf, lowerSemicontinuous_iff_isClosed_epigraph, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
inst : TopologicalSpace α
β : Type u_5
f : α → β
s : Set α
inst_1 : Preorder β
⊢ UpperSemicontinuousOn f s ↔ ∀ (b : β), ∃ (u : Set α), IsOpen[inst] u ∧ s ∩ f ⁻¹' Iio b = s ∩ u

Tactic:
lowerSemicontinuousOn_iff_preimage_Ioi (β := βᵒᵈ)

Premises used: setOf, lowerSemicontinuousOn_iff_preimage_Ioi, OrderDual, Set.Iio
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
inst : TopologicalSpace α
β : Type u_5
f : α → β
s : Set α
inst_1 : LinearOrder β
⊢ UpperSemicontinuousOn f s ↔ ∀ (b : β), ∃ (v : Set α), IsClosed[inst] v ∧ s ∩ f ⁻¹' Ici b = s ∩ v

Tactic:
lowerSemicontinuousOn_iff_preimage_Iic (γ := βᵒᵈ)

Premises used: Set.Ici, setOf, lowerSemicontinuousOn_iff_preimage_Iic, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
inst : TopologicalSpace α
β : Type u_5
f : α → β
s : Set α
a : α
inst_1 : PartialOrder β
inst_2 : CommGroup β
inst_3 : IsOrderedMonoid β
rw :
  (∀ (x : β), x⁻¹ < f⁻¹ a → ∀ᶠ (x' : α) in 𝓝[s] a, x⁻¹ < f⁻¹ x') ↔ ∀ (y : β), f a < y → ∀ᶠ (x' : α) in 𝓝[s] a, f x' < y
⊢ LowerSemicontinuousWithinAt f⁻¹ s a ↔ UpperSemicontinuousWithinAt f s a

Tactic:
rw [lowerSemicontinuousWithinAt_iff, inv_surjective.forall, upperSemicontinuousWithinAt_iff]

Premises used: inv_surjective, Function.Surjective.forall, lowerSemicontinuousWithinAt_iff, upperSemicontinuousWithinAt_iff
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
inst : TopologicalSpace α
β : Type u_5
f : α → β
s : Set α
a : α
inst_1 : PartialOrder β
inst_2 : CommGroup β
inst_3 : IsOrderedMonoid β
⊢ (∀ (x : β), x⁻¹ < f⁻¹ a → ∀ᶠ (x' : α) in 𝓝[s] a, x⁻¹ < f⁻¹ x') ↔ ∀ (y : β), f a < y → ∀ᶠ (x' : α) in 𝓝[s] a, f x' < y

Tactic:
simp
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
inst : TopologicalSpace α
β : Type u_5
f : α → β
s : Set α
a : α
inst_1 : PartialOrder β
inst_2 : CommGroup β
inst_3 : IsOrderedMonoid β
⊢ UpperSemicontinuousWithinAt f⁻¹ s a ↔ LowerSemicontinuousWithinAt f s a

Tactic:
simp [← lowerSemicontinuousWithinAt_inv_iff]

Premises used: lowerSemicontinuousWithinAt_inv_iff
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
inst : TopologicalSpace α
β : Type u_5
f : α → β
a : α
inst_1 : PartialOrder β
inst_2 : CommGroup β
inst_3 : IsOrderedMonoid β
⊢ LowerSemicontinuousAt f⁻¹ a ↔ UpperSemicontinuousAt f a

Tactic:
simp [← lowerSemicontinuousWithinAt_univ_iff, ← upperSemicontinuousWithinAt_univ_iff]

Premises used: lowerSemicontinuousWithinAt_univ_iff, upperSemicontinuousWithinAt_univ_iff
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
inst : TopologicalSpace α
β : Type u_5
f : α → β
a : α
inst_1 : PartialOrder β
inst_2 : CommGroup β
inst_3 : IsOrderedMonoid β
⊢ UpperSemicontinuousAt f⁻¹ a ↔ LowerSemicontinuousAt f a

Tactic:
simp [← lowerSemicontinuousWithinAt_univ_iff, ← upperSemicontinuousWithinAt_univ_iff]

Premises used: lowerSemicontinuousWithinAt_univ_iff, upperSemicontinuousWithinAt_univ_iff
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
inst : TopologicalSpace α
β : Type u_5
f : α → β
s : Set α
inst_1 : PartialOrder β
inst_2 : CommGroup β
inst_3 : IsOrderedMonoid β
⊢ LowerSemicontinuousOn f⁻¹ s ↔ UpperSemicontinuousOn f s

Tactic:
simp [lowerSemicontinuousOn_iff, upperSemicontinuousOn_iff]

Premises used: lowerSemicontinuousOn_iff, upperSemicontinuousOn_iff
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
inst : TopologicalSpace α
β : Type u_5
f : α → β
s : Set α
inst_1 : PartialOrder β
inst_2 : CommGroup β
inst_3 : IsOrderedMonoid β
⊢ UpperSemicontinuousOn f⁻¹ s ↔ LowerSemicontinuousOn f s

Tactic:
simp [← lowerSemicontinuousOn_inv_iff]

Premises used: lowerSemicontinuousOn_inv_iff
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
inst : TopologicalSpace α
β : Type u_5
f : α → β
inst_1 : PartialOrder β
inst_2 : CommGroup β
inst_3 : IsOrderedMonoid β
⊢ LowerSemicontinuous f⁻¹ ↔ UpperSemicontinuous f

Tactic:
simp [← upperSemicontinuousOn_univ_iff, ← lowerSemicontinuousOn_univ_iff]

Premises used: lowerSemicontinuousOn_univ_iff, upperSemicontinuousOn_univ_iff
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_4
inst : TopologicalSpace α
β : Type u_5
f : α → β
inst_1 : PartialOrder β
inst_2 : CommGroup β
inst_3 : IsOrderedMonoid β
⊢ UpperSemicontinuous f⁻¹ ↔ LowerSemicontinuous f

Tactic:
simp [← upperSemicontinuousOn_univ_iff, ← lowerSemicontinuousOn_univ_iff]

Premises used: lowerSemicontinuousOn_univ_iff, upperSemicontinuousOn_univ_iff
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : UpperSemicontinuousWithinAt f s x
gmon : Monotone g
⊢ UpperSemicontinuousWithinAt (g ∘ f) s x

Tactic:
ContinuousAt.comp_lowerSemicontinuousWithinAt (γ := γᵒᵈ) (δ := δᵒᵈ) hg hf gmon.dual

Premises used: ContinuousAt.comp_lowerSemicontinuousWithinAt, Monotone.dual, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : UpperSemicontinuousAt f x
gmon : Monotone g
⊢ UpperSemicontinuousAt (g ∘ f) x

Tactic:
ContinuousAt.comp_lowerSemicontinuousAt (γ := γᵒᵈ) (δ := δᵒᵈ) hg hf gmon.dual

Premises used: ContinuousAt.comp_lowerSemicontinuousAt, Monotone.dual, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : Continuous[inst_2, inst_5] g
hf : UpperSemicontinuousOn f s
gmon : Monotone g
⊢ UpperSemicontinuousOn (g ∘ f) s

Tactic:
fun x hx => hg.continuousAt.comp_upperSemicontinuousWithinAt (hf x hx) gmon

Premises used: ContinuousAt.comp_upperSemicontinuousWithinAt, Continuous.continuousAt, SemicontinuousOn
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : Continuous[inst_2, inst_5] g
hf : UpperSemicontinuous f
gmon : Monotone g
⊢ UpperSemicontinuous (g ∘ f)

Tactic:
fun x =>
  hg.continuousAt.comp_upperSemicontinuousAt (hf x) gmon

Premises used: ContinuousAt.comp_upperSemicontinuousAt, Continuous.continuousAt, Semicontinuous
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : UpperSemicontinuousWithinAt f s x
gmon : Antitone g
⊢ LowerSemicontinuousWithinAt (g ∘ f) s x

Tactic:
ContinuousAt.comp_upperSemicontinuousWithinAt (δ := δᵒᵈ) hg hf gmon

Premises used: ContinuousAt.comp_upperSemicontinuousWithinAt, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : UpperSemicontinuousAt f x
gmon : Antitone g
⊢ LowerSemicontinuousAt (g ∘ f) x

Tactic:
ContinuousAt.comp_upperSemicontinuousAt (δ := δᵒᵈ) hg hf gmon

Premises used: ContinuousAt.comp_upperSemicontinuousAt, OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : Continuous[inst_2, inst_5] g
hf : UpperSemicontinuousOn f s
gmon : Antitone g
⊢ LowerSemicontinuousOn (g ∘ f) s

Tactic:
fun x hx => hg.continuousAt.comp_upperSemicontinuousWithinAt_antitone (hf x hx) gmon

Premises used: Continuous.continuousAt, ContinuousAt.comp_upperSemicontinuousWithinAt_antitone, SemicontinuousOn
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : Continuous[inst_2, inst_5] g
hf : UpperSemicontinuous f
gmon : Antitone g
⊢ LowerSemicontinuous (g ∘ f)

Tactic:
fun x =>
  hg.continuousAt.comp_upperSemicontinuousAt_antitone (hf x) gmon

Premises used: ContinuousAt.comp_upperSemicontinuousAt_antitone, Continuous.continuousAt, Semicontinuous
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst_1 : AddCommMonoid γ
inst_2 : LinearOrder γ
inst_3 : IsOrderedAddMonoid γ
inst_4 : TopologicalSpace γ
inst_5 : OrderTopology γ
f g : α → γ
hf : UpperSemicontinuousWithinAt f s x
hg : UpperSemicontinuousWithinAt g s x
hcont : ContinuousAt (Y := γ) (fun (p : γ × γ) ↦ p.1 + p.2) (f x, g x)
⊢ UpperSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ f z + g z) s x

Tactic:
LowerSemicontinuousWithinAt.add' (γ := γᵒᵈ) hf hg hcont

Premises used: LowerSemicontinuousWithinAt.add', OrderDual
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
γ : Type u_5
inst_1 : AddCommMonoid γ
inst_2 : LinearOrder γ
inst_3 : IsOrderedAddMonoid γ
inst_4 : TopologicalSpace γ
inst_5 : OrderTopology γ
f g : α → γ
hf : UpperSemicontinuousAt f x
hg : UpperSemicontinuousAt g x
hcont : ContinuousAt (Y := γ) (fun (p : γ × γ) ↦ p.1 + p.2) (f x, g x)
simp_rw :
  ∀ (hf : UpperSemicontinuousWithinAt f univ x) (hg : UpperSemicontinuousWithinAt g univ x),
    UpperSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ f z + g z) univ x
⊢ UpperSemicontinuousAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ f z + g z) x

Tactic:
simp_rw [← upperSemicontinuousWithinAt_univ_iff] at *

Premises used: upperSemicontinuousWithinAt_univ_iff
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
γ : Type u_5
inst_1 : AddCommMonoid γ
inst_2 : LinearOrder γ
inst_3 : IsOrderedAddMonoid γ
inst_4 : TopologicalSpace γ
inst_5 : OrderTopology γ
f g : α → γ
hcont : ContinuousAt (Y := γ) (fun (p : γ × γ) ↦ p.1 + p.2) (f x, g x)
hf : UpperSemicontinuousWithinAt f univ x
hg : UpperSemicontinuousWithinAt g univ x
⊢ UpperSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ f z + g z) univ x

Tactic:
hf.add' hg hcont

Premises used: UpperSemicontinuousWithinAt.add'
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
γ : Type u_5
inst_1 : AddCommMonoid γ
inst_2 : LinearOrder γ
inst_3 : IsOrderedAddMonoid γ
inst_4 : TopologicalSpace γ
inst_5 : OrderTopology γ
f g : α → γ
hcont : ContinuousAt (Y := γ) (fun (p : γ × γ) ↦ p.1 + p.2) (f x, g x)
hf : UpperSemicontinuousWithinAt f univ x
hg : UpperSemicontinuousWithinAt g univ x
⊢ UpperSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ f z + g z) univ x

Tactic:
exact hf.add' hg hcont

Premises used: UpperSemicontinuousWithinAt.add'