text:
/-
Copyright (c) 2021 Oliver Nash. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Oliver Nash

! This file was ported from Lean 3 source module topology.uniform_space.compact_convergence
! leanprover-community/mathlib commit dc6c365e751e34d100e80fe6e314c3c3e0fd2988
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Topology.CompactOpen
import Mathlib.Topology.UniformSpace.UniformConvergence

/-!
# Compact convergence (uniform convergence on compact sets)

Given a topological space `α` and a uniform space `β` (e.g., a metric space or a topological group),
the space of continuous maps `C(α, β)` carries a natural uniform space structure. We define this
uniform space structure in this file and also prove the following properties of the topology it
induces on `C(α, β)`:

 1. Given a sequence of continuous functions `Fₙ : α → β` together with some continuous `f : α → β`,
    then `Fₙ` converges to `f` as a sequence in `C(α, β)` iff `Fₙ` converges to `f` uniformly on
    each compact subset `K` of `α`.
 2. Given `Fₙ` and `f` as above and suppose `α` is locally compact, then `Fₙ` converges to `f` iff
    `Fₙ` converges to `f` locally uniformly.
 3. The topology coincides with the compact-open topology.

Property 1 is essentially true by definition, 2 follows from basic results about uniform
convergence, but 3 requires a little work and uses the Lebesgue number lemma.

## The uniform space structure

Given subsets `K ⊆ α` and `V ⊆ β × β`, let `E(K, V) ⊆ C(α, β) × C(α, β)` be the set of pairs of
continuous functions `α → β` which are `V`-close on `K`:
$$
  E(K, V) = \{ (f, g) | ∀ (x ∈ K), (f x, g x) ∈ V \}.
$$
Fixing some `f ∈ C(α, β)`, let `N(K, V, f) ⊆ C(α, β)` be the set of continuous functions `α → β`
which are `V`-close to `f` on `K`:
$$
  N(K, V, f) = \{ g | ∀ (x ∈ K), (f x, g x) ∈ V \}.
$$
Using this notation we can describe the uniform space structure and the topology it induces.
Specifically:
 *  A subset `X ⊆ C(α, β) × C(α, β)` is an entourage for the uniform space structure on `C(α, β)`
    iff there exists a compact `K` and entourage `V` such that `E(K, V) ⊆ X`.
 *  A subset `Y ⊆ C(α, β)` is a neighbourhood of `f` iff there exists a compact `K` and entourage
    `V` such that `N(K, V, f) ⊆ Y`.

The topology on `C(α, β)` thus has a natural subbasis (the compact-open subbasis) and a natural
neighbourhood basis (the compact-convergence neighbourhood basis).

## Main definitions / results

 * `ContinuousMap.compactOpen_eq_compactConvergence`: the compact-open topology is equal to the
   compact-convergence topology.
 * `ContinuousMap.compactConvergenceUniformSpace`: the uniform space structure on `C(α, β)`.
 * `ContinuousMap.mem_compactConvergence_entourage_iff`: a characterisation of the entourages
    of `C(α, β)`.
 * `ContinuousMap.tendsto_iff_forall_compact_tendstoUniformlyOn`: a sequence of functions `Fₙ` in
    `C(α, β)` converges to some `f` iff `Fₙ` converges to `f` uniformly on each compact subset
    `K` of `α`.
 * `ContinuousMap.tendsto_iff_tendstoLocallyUniformly`: on a locally compact space, a sequence of
    functions `Fₙ` in `C(α, β)` converges to some `f` iff `Fₙ` converges to `f` locally uniformly.
 * `ContinuousMap.tendsto_iff_tendstoUniformly`: on a compact space, a sequence of functions `Fₙ` in
    `C(α, β)` converges to some `f` iff `Fₙ` converges to `f` uniformly.

## Implementation details

We use the forgetful inheritance pattern (see Note [forgetful inheritance]) to make the topology
of the uniform space structure on `C(α, β)` definitionally equal to the compact-open topology.

## TODO

 * When `β` is a metric space, there is natural basis for the compact-convergence topology
   parameterised by triples `(K, ε, f)` for a real number `ε > 0`.
 * When `α` is compact and `β` is a metric space, the compact-convergence topology (and thus also
   the compact-open topology) is metrisable.
 * Results about uniformly continuous functions `γ → C(α, β)` and uniform limits of sequences
   `ι → γ → C(α, β)`.
-/

universe u₁ u₂ u₃

open Filter Uniformity Topology

open UniformSpace Set Filter

variable {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β]

variable (K : Set α) (V : Set (β × β)) (f : C(α, β))

namespace ContinuousMap

/-- Given `K ⊆ α`, `V ⊆ β × β`, and `f : C(α, β)`, we define `ContinuousMap.compactConvNhd K V f`
to be the set of `g : C(α, β)` that are `V`-close to `f` on `K`. -/
def compactConvNhd : Set C(α, β) :=
  { g | ∀ x ∈ K, (f x, g x) ∈ V }
#align continuous_map.compact_conv_nhd ContinuousMap.compactConvNhd

variable {K V}

theorem self_mem_compactConvNhd (hV : V ∈ 𝓤 β) : f ∈ compactConvNhd K V f := fun _x _hx =>
  refl_mem_uniformity hV
#align continuous_map.self_mem_compact_conv_nhd ContinuousMap.self_mem_compactConvNhd

@[mono]
theorem compactConvNhd_mono {V' : Set (β × β)} (hV' : V' ⊆ V) :
    compactConvNhd K V' f ⊆ compactConvNhd K V f := fun _x hx a ha => hV' (hx a ha)
#align continuous_map.compact_conv_nhd_mono ContinuousMap.compactConvNhd_mono

theorem compactConvNhd_mem_comp {g₁ g₂ : C(α, β)} {V' : Set (β × β)}
    (hg₁ : g₁ ∈ compactConvNhd K V f) (hg₂ : g₂ ∈ compactConvNhd K V' g₁) :
    g₂ ∈ compactConvNhd K (V ○ V') f := fun x hx => ⟨g₁ x, hg₁ x hx, hg₂ x hx⟩
#align continuous_map.compact_conv_nhd_mem_comp ContinuousMap.compactConvNhd_mem_comp

/-- A key property of `ContinuousMap.compactConvNhd`. It allows us to apply
`TopologicalSpace.nhds_mkOfNhds_filterBasis` below. -/
theorem compactConvNhd_nhd_basis (hV : V ∈ 𝓤 β) :
    ∃ V' ∈ 𝓤 β,
      V' ⊆ V ∧ ∀ g ∈ compactConvNhd K V' f, compactConvNhd K V' g ⊆ compactConvNhd K V f := by
  obtain ⟨V', h₁, h₂⟩ := comp_mem_uniformity_sets hV
  exact
    ⟨V', h₁, Subset.trans (subset_comp_self_of_mem_uniformity h₁) h₂, fun g hg g' hg' =>
      compactConvNhd_mono f h₂ (compactConvNhd_mem_comp f hg hg')⟩
#align continuous_map.compact_conv_nhd_nhd_basis ContinuousMap.compactConvNhd_nhd_basis

theorem compactConvNhd_subset_inter (K₁ K₂ : Set α) (V₁ V₂ : Set (β × β)) :
    compactConvNhd (K₁ ∪ K₂) (V₁ ∩ V₂) f ⊆ compactConvNhd K₁ V₁ f ∩ compactConvNhd K₂ V₂ f :=
  fun _g hg =>
  ⟨fun x hx => mem_of_mem_inter_left (hg x (mem_union_left K₂ hx)), fun x hx =>
    mem_of_mem_inter_right (hg x (mem_union_right K₁ hx))⟩
#align continuous_map.compact_conv_nhd_subset_inter ContinuousMap.compactConvNhd_subset_inter

theorem compactConvNhd_compact_entourage_nonempty :
    { KV : Set α × Set (β × β) | IsCompact KV.1 ∧ KV.2 ∈ 𝓤 β }.Nonempty :=
  ⟨⟨∅, univ⟩, isCompact_empty, Filter.univ_mem⟩
#align continuous_map.compact_conv_nhd_compact_entourage_nonempty ContinuousMap.compactConvNhd_compact_entourage_nonempty

theorem compactConvNhd_filter_isBasis :
    Filter.IsBasis (fun KV : Set α × Set (β × β) => IsCompact KV.1 ∧ KV.2 ∈ 𝓤 β) fun KV =>
      compactConvNhd KV.1 KV.2 f :=
  { nonempty := compactConvNhd_compact_entourage_nonempty
    inter := by
      rintro ⟨K₁, V₁⟩ ⟨K₂, V₂⟩ ⟨hK₁, hV₁⟩ ⟨hK₂, hV₂⟩
      exact
        ⟨⟨K₁ ∪ K₂, V₁ ∩ V₂⟩, ⟨hK₁.union hK₂, Filter.inter_mem hV₁ hV₂⟩,
          compactConvNhd_subset_inter f K₁ K₂ V₁ V₂⟩ }
#align continuous_map.compact_conv_nhd_filter_is_basis ContinuousMap.compactConvNhd_filter_isBasis

/-- A filter basis for the neighbourhood filter of a point in the compact-convergence topology. -/
def compactConvergenceFilterBasis (f : C(α, β)) : FilterBasis C(α, β) :=
  (compactConvNhd_filter_isBasis f).filterBasis
#align continuous_map.compact_convergence_filter_basis ContinuousMap.compactConvergenceFilterBasis

theorem mem_compactConvergence_nhd_filter (Y : Set C(α, β)) :
    Y ∈ (compactConvergenceFilterBasis f).filter ↔
      ∃ (K : Set α)(V : Set (β × β))(_hK : IsCompact K)(_hV : V ∈ 𝓤 β), compactConvNhd K V f ⊆ Y :=
  by
  constructor
  · rintro ⟨X, ⟨⟨K, V⟩, ⟨hK, hV⟩, rfl⟩, hY⟩
    exact ⟨K, V, hK, hV, hY⟩
  · rintro ⟨K, V, hK, hV, hY⟩
    exact ⟨compactConvNhd K V f, ⟨⟨K, V⟩, ⟨hK, hV⟩, rfl⟩, hY⟩
#align continuous_map.mem_compact_convergence_nhd_filter ContinuousMap.mem_compactConvergence_nhd_filter

/-- The compact-convergence topology. In fact, see `ContinuousMap.compactOpen_eq_compactConvergence`
this is the same as the compact-open topology. This definition is thus an auxiliary convenience
definition and is unlikely to be of direct use. -/
def compactConvergenceTopology : TopologicalSpace C(α, β) :=
  TopologicalSpace.mkOfNhds fun f => (compactConvergenceFilterBasis f).filter
#align continuous_map.compact_convergence_topology ContinuousMap.compactConvergenceTopology

theorem nhds_compactConvergence :
    @nhds _ compactConvergenceTopology f = (compactConvergenceFilterBasis f).filter := by
  rw [TopologicalSpace.nhds_mkOfNhds_filterBasis] <;> rintro g - ⟨⟨K, V⟩, ⟨hK, hV⟩, rfl⟩
  · exact self_mem_compactConvNhd g hV
  · obtain ⟨V', hV', h₁, h₂⟩ := compactConvNhd_nhd_basis g hV
    exact
      ⟨compactConvNhd K V' g, ⟨⟨K, V'⟩, ⟨hK, hV'⟩, rfl⟩, compactConvNhd_mono g h₁, fun g' hg' =>
        ⟨compactConvNhd K V' g', ⟨⟨K, V'⟩, ⟨hK, hV'⟩, rfl⟩, h₂ g' hg'⟩⟩
#align continuous_map.nhds_compact_convergence ContinuousMap.nhds_compactConvergence

theorem hasBasis_nhds_compactConvergence :
    HasBasis (@nhds _ compactConvergenceTopology f)
      (fun p : Set α × Set (β × β) => IsCompact p.1 ∧ p.2 ∈ 𝓤 β) fun p =>
      compactConvNhd p.1 p.2 f :=
  (nhds_compactConvergence f).symm ▸ (compactConvNhd_filter_isBasis f).hasBasis
#align continuous_map.has_basis_nhds_compact_convergence ContinuousMap.hasBasis_nhds_compactConvergence

/-- This is an auxiliary lemma and is unlikely to be of direct use outside of this file. See
`ContinuousMap.tendsto_iff_forall_compact_tendstoUniformlyOn` below for the useful version where the
topology is picked up via typeclass inference. -/
theorem tendsto_iff_forall_compact_tendstoUniformlyOn' {ι : Type u₃} {p : Filter ι}
    {F : ι → C(α, β)} :
    Filter.Tendsto F p (@nhds _ compactConvergenceTopology f) ↔
      ∀ K, IsCompact K → TendstoUniformlyOn (fun i a => F i a) f p K := by
  simp only [(hasBasis_nhds_compactConvergence f).tendsto_right_iff, TendstoUniformlyOn, and_imp,
    Prod.forall]
  refine' forall_congr' fun K => _
  rw [forall_swap]
  exact forall₃_congr fun _hK V _hV => Iff.rfl
#align continuous_map.tendsto_iff_forall_compact_tendsto_uniformly_on' ContinuousMap.tendsto_iff_forall_compact_tendstoUniformlyOn'

/-- Any point of `ContinuousMap.CompactOpen.gen K U` is also an interior point wrt the topology of
compact convergence.

The topology of compact convergence is thus at least as fine as the compact-open topology. -/
theorem compactConvNhd_subset_compactOpen (hK : IsCompact K) {U : Set β} (hU : IsOpen U)
    (hf : f ∈ CompactOpen.gen K U) :
    ∃ V ∈ 𝓤 β, IsOpen V ∧ compactConvNhd K V f ⊆ CompactOpen.gen K U := by
  obtain ⟨V, hV₁, hV₂, hV₃⟩ := lebesgue_number_of_compact_open (hK.image f.continuous) hU hf
  refine' ⟨V, hV₁, hV₂, _⟩
  rintro g hg _ ⟨x, hx, rfl⟩
  exact hV₃ (f x) ⟨x, hx, rfl⟩ (hg x hx)
#align continuous_map.compact_conv_nhd_subset_compact_open ContinuousMap.compactConvNhd_subset_compactOpen

/-- The point `f` in `ContinuousMap.compactConvNhd K V f` is also an interior point wrt the
compact-open topology.

Since `ContinuousMap.compactConvNhd K V f` are a neighbourhood basis at `f` for each `f`, it follows
that the compact-open topology is at least as fine as the topology of compact convergence. -/
theorem interᵢ_compactOpen_gen_subset_compactConvNhd (hK : IsCompact K) (hV : V ∈ 𝓤 β) :
    ∃ (ι : Sort (u₁ + 1))(_ : Fintype ι)(C : ι → Set α)(_hC : ∀ i, IsCompact (C i))(U :
      ι → Set β)(_hU : ∀ i, IsOpen (U i)),
      (f ∈ ⋂ i, CompactOpen.gen (C i) (U i)) ∧
        (⋂ i, CompactOpen.gen (C i) (U i)) ⊆ compactConvNhd K V f := by
  obtain ⟨W, hW₁, hW₄, hW₂, hW₃⟩ := comp_open_symm_mem_uniformity_sets hV
  obtain ⟨Z, hZ₁, hZ₄, hZ₂, hZ₃⟩ := comp_open_symm_mem_uniformity_sets hW₁
  let U : α → Set α := fun x => f ⁻¹' ball (f x) Z
  have hU : ∀ x, IsOpen (U x) := fun x => f.continuous.isOpen_preimage _ (isOpen_ball _ hZ₄)
  have hUK : K ⊆ ⋃ x : K, U (x : K) := by
    intro x hx
    simp only [exists_prop, mem_unionᵢ, unionᵢ_coe_set, mem_preimage]
    exact ⟨(⟨x, hx⟩ : K), by simp [hx, mem_ball_self (f x) hZ₁]⟩
  obtain ⟨t, ht⟩ := hK.elim_finite_subcover _ (fun x : K => hU x.val) hUK
  let C : t → Set α := fun i => K ∩ closure (U ((i : K) : α))
  have hC : K ⊆ ⋃ i, C i := by
    rw [← K.inter_unionᵢ, subset_inter_iff]
    refine' ⟨Subset.rfl, ht.trans _⟩
    simp only [SetCoe.forall, Subtype.coe_mk, unionᵢ_subset_iff]
    exact fun x hx₁ hx₂ => subset_unionᵢ_of_subset (⟨_, hx₂⟩ : t) (by simp [subset_closure])
  have hfC : ∀ i : t, C i ⊆ f ⁻¹' ball (f ((i : K) : α)) W :=
    by
    simp only [← image_subset_iff, ← mem_preimage]
    rintro ⟨⟨x, hx₁⟩, hx₂⟩
    have hZW : closure (ball (f x) Z) ⊆ ball (f x) W :=
      by
      intro y hy
      obtain ⟨z, hz₁, hz₂⟩ := UniformSpace.mem_closure_iff_ball.mp hy hZ₁
      exact ball_mono hZ₃ _ (mem_ball_comp hz₂ ((mem_ball_symmetry hZ₂).mp hz₁))
    calc
      f '' (K ∩ closure (U x)) ⊆ f '' closure (U x) := image_subset _ (inter_subset_right _ _)
      _ ⊆ closure (f '' U x) := f.continuous.continuousOn.image_closure
      _ ⊆ closure (ball (f x) Z) :=
        by
          apply closure_mono
          simp only [image_subset_iff]
          rfl
      _ ⊆ ball (f x) W := hZW

  refine'
    ⟨t, t.fintypeCoeSort, C, fun i => hK.inter_right isClosed_closure, fun i =>
      ball (f ((i : K) : α)) W, fun i => isOpen_ball _ hW₄, by simp [CompactOpen.gen, hfC],
      fun g hg x hx => hW₃ (mem_compRel.mpr _)⟩
  simp only [mem_interᵢ, CompactOpen.gen, mem_setOf_eq, image_subset_iff] at hg
  obtain ⟨y, hy⟩ := mem_unionᵢ.mp (hC hx)
  exact ⟨f y, (mem_ball_symmetry hW₂).mp (hfC y hy), mem_preimage.mp (hg y hy)⟩
#align continuous_map.Inter_compact_open_gen_subset_compact_conv_nhd ContinuousMap.interᵢ_compactOpen_gen_subset_compactConvNhd

/-- The compact-open topology is equal to the compact-convergence topology. -/
theorem compactOpen_eq_compactConvergence :
    ContinuousMap.compactOpen = (compactConvergenceTopology : TopologicalSpace C(α, β)) := by
  rw [compactConvergenceTopology, ContinuousMap.compactOpen]
  refine' le_antisymm _ _
  · refine' fun X hX => isOpen_iff_forall_mem_open.mpr fun f hf => _
    have hXf : X ∈ (compactConvergenceFilterBasis f).filter :=
      by
      rw [← nhds_compactConvergence]
      exact @IsOpen.mem_nhds C(α, β) compactConvergenceTopology _ _ hX hf
    obtain ⟨-, ⟨⟨K, V⟩, ⟨hK, hV⟩, rfl⟩, hXf⟩ := hXf
    obtain ⟨ι, hι, C, hC, U, hU, h₁, h₂⟩ := interᵢ_compactOpen_gen_subset_compactConvNhd f hK hV
    haveI := hι
    exact
      ⟨⋂ i, CompactOpen.gen (C i) (U i), h₂.trans hXf,
        isOpen_interᵢ fun i => ContinuousMap.isOpen_gen (hC i) (hU i), h₁⟩
  · simp only [TopologicalSpace.le_generateFrom_iff_subset_isOpen, and_imp, exists_prop,
      forall_exists_index, setOf_subset_setOf]
    rintro - K hK U hU rfl f hf
    obtain ⟨V, hV, _hV', hVf⟩ := compactConvNhd_subset_compactOpen f hK hU hf
    exact Filter.mem_of_superset (FilterBasis.mem_filter_of_mem _ ⟨⟨K, V⟩, ⟨hK, hV⟩, rfl⟩) hVf
#align continuous_map.compact_open_eq_compact_convergence ContinuousMap.compactOpen_eq_compactConvergence

/-- The filter on `C(α, β) × C(α, β)` which underlies the uniform space structure on `C(α, β)`. -/
def compactConvergenceUniformity : Filter (C(α, β) × C(α, β)) :=
  ⨅ KV ∈ { KV : Set α × Set (β × β) | IsCompact KV.1 ∧ KV.2 ∈ 𝓤 β },
    𝓟 { fg : C(α, β) × C(α, β) | ∀ x : α, x ∈ KV.1 → (fg.1 x, fg.2 x) ∈ KV.2 }
#align continuous_map.compact_convergence_uniformity ContinuousMap.compactConvergenceUniformity

theorem hasBasis_compactConvergenceUniformity_aux :
    HasBasis (@compactConvergenceUniformity α β _ _)
      (fun p : Set α × Set (β × β) => IsCompact p.1 ∧ p.2 ∈ 𝓤 β) fun p =>
      { fg : C(α, β) × C(α, β) | ∀ x ∈ p.1, (fg.1 x, fg.2 x) ∈ p.2 } := by
  refine' Filter.hasBasis_binfᵢ_principal _ compactConvNhd_compact_entourage_nonempty
  rintro ⟨K₁, V₁⟩ ⟨hK₁, hV₁⟩ ⟨K₂, V₂⟩ ⟨hK₂, hV₂⟩
  refine' ⟨⟨K₁ ∪ K₂, V₁ ∩ V₂⟩, ⟨hK₁.union hK₂, Filter.inter_mem hV₁ hV₂⟩, _⟩
  simp only [le_eq_subset, Prod.forall, setOf_subset_setOf, ge_iff_le, Order.Preimage, ←
    forall_and, mem_inter_iff, mem_union]
  exact fun f g => forall_imp fun x => by tauto
#align continuous_map.has_basis_compact_convergence_uniformity_aux ContinuousMap.hasBasis_compactConvergenceUniformity_aux

/-- An intermediate lemma. Usually `ContinuousMap.mem_compactConvergence_entourage_iff` is more
useful. -/
theorem mem_compactConvergenceUniformity (X : Set (C(α, β) × C(α, β))) :
    X ∈ @compactConvergenceUniformity α β _ _ ↔
      ∃ (K : Set α)(V : Set (β × β))(_hK : IsCompact K)(_hV : V ∈ 𝓤 β),
        { fg : C(α, β) × C(α, β) | ∀ x ∈ K, (fg.1 x, fg.2 x) ∈ V } ⊆ X := by
  simp only [hasBasis_compactConvergenceUniformity_aux.mem_iff, exists_prop, Prod.exists,
    and_assoc]
#align continuous_map.mem_compact_convergence_uniformity ContinuousMap.mem_compactConvergenceUniformity

/-- Note that we ensure the induced topology is definitionally the compact-open topology. -/
instance compactConvergenceUniformSpace : UniformSpace C(α, β)
    where
  uniformity := compactConvergenceUniformity
  refl :=
    by
    simp only [compactConvergenceUniformity, and_imp, Filter.le_principal_iff, Prod.forall,
      Filter.mem_principal, mem_setOf_eq, le_infᵢ_iff, idRel_subset]
    exact fun K V _hK hV f x _hx => refl_mem_uniformity hV
  symm :=
    by
    simp only [compactConvergenceUniformity, and_imp, Prod.forall, mem_setOf_eq, Prod.fst_swap,
      Filter.tendsto_principal, Prod.snd_swap, Filter.tendsto_infᵢ]
    intro K V hK hV
    obtain ⟨V', hV', hsymm, hsub⟩ := symm_of_uniformity hV
    let X := { fg : C(α, β) × C(α, β) | ∀ x : α, x ∈ K → (fg.1 x, fg.2 x) ∈ V' }
    have hX : X ∈ compactConvergenceUniformity :=
      (mem_compactConvergenceUniformity X).mpr ⟨K, V', hK, hV', by simp⟩
    exact Filter.eventually_of_mem hX fun fg hfg x hx => hsub (hsymm _ _ (hfg x hx))
  comp X hX :=
    by
    obtain ⟨K, V, hK, hV, hX⟩ := (mem_compactConvergenceUniformity X).mp hX
    obtain ⟨V', hV', hcomp⟩ := comp_mem_uniformity_sets hV
    let h := fun s : Set (C(α, β) × C(α, β)) => s ○ s
    suffices
      h { fg : C(α, β) × C(α, β) | ∀ x ∈ K, (fg.1 x, fg.2 x) ∈ V' } ∈
        compactConvergenceUniformity.lift' h
      by
      apply Filter.mem_of_superset this
      rintro ⟨f, g⟩ ⟨z, hz₁, hz₂⟩
      refine' hX fun x hx => hcomp _
      exact ⟨z x, hz₁ x hx, hz₂ x hx⟩
    apply Filter.mem_lift'
    exact (mem_compactConvergenceUniformity _).mpr ⟨K, V', hK, hV', Subset.refl _⟩
  isOpen_uniformity := by
    rw [compactOpen_eq_compactConvergence]
    refine' fun Y => forall₂_congr fun f hf => _
    simp only [mem_compactConvergence_nhd_filter, mem_compactConvergenceUniformity, Prod.forall,
      setOf_subset_setOf, compactConvNhd]
    refine' exists₄_congr fun K V _hK _hV => ⟨_, fun hY g hg => hY f g hg rfl⟩
    rintro hY g₁ g₂ hg₁ rfl
    exact hY hg₁
#align continuous_map.compact_convergence_uniform_space ContinuousMap.compactConvergenceUniformSpace

theorem mem_compactConvergence_entourage_iff (X : Set (C(α, β) × C(α, β))) :
    X ∈ 𝓤 C(α, β) ↔
      ∃ (K : Set α)(V : Set (β × β))(_hK : IsCompact K)(_hV : V ∈ 𝓤 β),
        { fg : C(α, β) × C(α, β) | ∀ x ∈ K, (fg.1 x, fg.2 x) ∈ V } ⊆ X :=
  mem_compactConvergenceUniformity X
#align continuous_map.mem_compact_convergence_entourage_iff ContinuousMap.mem_compactConvergence_entourage_iff

theorem hasBasis_compactConvergenceUniformity :
    HasBasis (𝓤 C(α, β)) (fun p : Set α × Set (β × β) => IsCompact p.1 ∧ p.2 ∈ 𝓤 β) fun p =>
      { fg : C(α, β) × C(α, β) | ∀ x ∈ p.1, (fg.1 x, fg.2 x) ∈ p.2 } :=
  hasBasis_compactConvergenceUniformity_aux
#align continuous_map.has_basis_compact_convergence_uniformity ContinuousMap.hasBasis_compactConvergenceUniformity

theorem _root_.Filter.HasBasis.compactConvergenceUniformity {ι : Type _} {pi : ι → Prop}
    {s : ι → Set (β × β)} (h : (𝓤 β).HasBasis pi s) :
    HasBasis (𝓤 C(α, β)) (fun p : Set α × ι => IsCompact p.1 ∧ pi p.2) fun p =>
      { fg : C(α, β) × C(α, β) | ∀ x ∈ p.1, (fg.1 x, fg.2 x) ∈ s p.2 } := by
  refine' hasBasis_compactConvergenceUniformity.to_hasBasis _ _
  · rintro ⟨t₁, t₂⟩ ⟨h₁, h₂⟩
    rcases h.mem_iff.1 h₂ with ⟨i, hpi, hi⟩
    exact ⟨(t₁, i), ⟨h₁, hpi⟩, fun fg hfg x hx => hi (hfg _ hx)⟩
  · rintro ⟨t, i⟩ ⟨ht, hi⟩
    exact ⟨(t, s i), ⟨ht, h.mem_of_mem hi⟩, Subset.rfl⟩
#align filter.has_basis.compact_convergence_uniformity Filter.HasBasis.compactConvergenceUniformity

variable {ι : Type u₃} {p : Filter ι} {F : ι → C(α, β)} {f}

theorem tendsto_iff_forall_compact_tendstoUniformlyOn :
    Tendsto F p (𝓝 f) ↔ ∀ K, IsCompact K → TendstoUniformlyOn (fun i a => F i a) f p K := by
  rw [compactOpen_eq_compactConvergence, tendsto_iff_forall_compact_tendstoUniformlyOn']
#align continuous_map.tendsto_iff_forall_compact_tendsto_uniformly_on ContinuousMap.tendsto_iff_forall_compact_tendstoUniformlyOn

/-- Locally uniform convergence implies convergence in the compact-open topology. -/
theorem tendsto_of_tendstoLocallyUniformly (h : TendstoLocallyUniformly (fun i a => F i a) f p) :
    Tendsto F p (𝓝 f) := by
  rw [tendsto_iff_forall_compact_tendstoUniformlyOn]
  intro K hK
  rw [← tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact hK]
  exact h.tendstoLocallyUniformlyOn
#align continuous_map.tendsto_of_tendsto_locally_uniformly ContinuousMap.tendsto_of_tendstoLocallyUniformly

/-- If every point has a compact neighbourhood, then convergence in the compact-open topology
implies locally uniform convergence.

See also `ContinuousMap.tendsto_iff_tendstoLocallyUniformly`, especially for T2 spaces. -/
theorem tendstoLocallyUniformly_of_tendsto (hα : ∀ x : α, ∃ n, IsCompact n ∧ n ∈ 𝓝 x)
    (h : Tendsto F p (𝓝 f)) : TendstoLocallyUniformly (fun i a => F i a) f p := by
  rw [tendsto_iff_forall_compact_tendstoUniformlyOn] at h
  intro V hV x
  obtain ⟨n, hn₁, hn₂⟩ := hα x
  exact ⟨n, hn₂, h n hn₁ V hV⟩
#align continuous_map.tendsto_locally_uniformly_of_tendsto ContinuousMap.tendstoLocallyUniformly_of_tendsto

/-- Convergence in the compact-open topology is the same as locally uniform convergence on a locally
compact space.

For non-T2 spaces, the assumption `LocallyCompactSpace α` is stronger than we need and in fact
the `←` direction is true unconditionally. See `ContinuousMap.tendstoLocallyUniformly_of_tendsto`
and `ContinuousMap.tendsto_of_tendstoLocallyUniformly` for versions requiring weaker hypotheses. -/
theorem tendsto_iff_tendstoLocallyUniformly [LocallyCompactSpace α] :
    Tendsto F p (𝓝 f) ↔ TendstoLocallyUniformly (fun i a => F i a) f p :=
  ⟨tendstoLocallyUniformly_of_tendsto exists_compact_mem_nhds, tendsto_of_tendstoLocallyUniformly⟩
#align continuous_map.tendsto_iff_tendsto_locally_uniformly ContinuousMap.tendsto_iff_tendstoLocallyUniformly

section CompactDomain

variable [CompactSpace α]

theorem hasBasis_compactConvergenceUniformity_of_compact :
    HasBasis (𝓤 C(α, β)) (fun V : Set (β × β) => V ∈ 𝓤 β) fun V =>
      { fg : C(α, β) × C(α, β) | ∀ x, (fg.1 x, fg.2 x) ∈ V } :=
  hasBasis_compactConvergenceUniformity.to_hasBasis
    (fun p hp => ⟨p.2, hp.2, fun _fg hfg x _hx => hfg x⟩) fun V hV =>
    ⟨⟨univ, V⟩, ⟨isCompact_univ, hV⟩, fun _fg hfg x => hfg x (mem_univ x)⟩
#align continuous_map.has_basis_compact_convergence_uniformity_of_compact ContinuousMap.hasBasis_compactConvergenceUniformity_of_compact

/-- Convergence in the compact-open topology is the same as uniform convergence for sequences of
continuous functions on a compact space. -/
theorem tendsto_iff_tendstoUniformly :
    Tendsto F p (𝓝 f) ↔ TendstoUniformly (fun i a => F i a) f p := by
  rw [tendsto_iff_forall_compact_tendstoUniformlyOn, ← tendstoUniformlyOn_univ]
  exact ⟨fun h => h univ isCompact_univ, fun h K _hK => h.mono (subset_univ K)⟩
#align continuous_map.tendsto_iff_tendsto_uniformly ContinuousMap.tendsto_iff_tendstoUniformly

end CompactDomain

end ContinuousMap


text:
/-
Copyright (c) 2018 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl
-/
import tactic.basic
import logic.relator

/-!
# Relation closures

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.

This file defines the reflexive, transitive, and reflexive transitive closures of relations.
It also proves some basic results on definitions in core, such as `eqv_gen`.

Note that this is about unbundled relations, that is terms of types of the form `α → β → Prop`. For
the bundled version, see `rel`.

## Definitions

* `relation.refl_gen`: Reflexive closure. `refl_gen r` relates everything `r` related, plus for all
  `a` it relates `a` with itself. So `refl_gen r a b ↔ r a b ∨ a = b`.
* `relation.trans_gen`: Transitive closure. `trans_gen r` relates everything `r` related
  transitively. So `trans_gen r a b ↔ ∃ x₀ ... xₙ, r a x₀ ∧ r x₀ x₁ ∧ ... ∧ r xₙ b`.
* `relation.refl_trans_gen`: Reflexive transitive closure. `refl_trans_gen r` relates everything
  `r` related transitively, plus for all `a` it relates `a` with itself. So
  `refl_trans_gen r a b ↔ (∃ x₀ ... xₙ, r a x₀ ∧ r x₀ x₁ ∧ ... ∧ r xₙ b) ∨ a = b`. It is the same as
  the reflexive closure of the transitive closure, or the transitive closure of the reflexive
  closure. In terms of rewriting systems, this means that `a` can be rewritten to `b` in a number of
  rewrites.
* `relation.comp`:  Relation composition. We provide notation `∘r`. For `r : α → β → Prop` and
  `s : β → γ → Prop`, `r ∘r s`relates `a : α` and `c : γ` iff there exists `b : β` that's related to
  both.
* `relation.map`: Image of a relation under a pair of maps. For `r : α → β → Prop`, `f : α → γ`,
  `g : β → δ`, `map r f g` is the relation `γ → δ → Prop` relating `f a` and `g b` for all `a`, `b`
  related by `r`.
* `relation.join`: Join of a relation. For `r : α → α → Prop`, `join r a b ↔ ∃ c, r a c ∧ r b c`. In
  terms of rewriting systems, this means that `a` and `b` can be rewritten to the same term.
-/

open function

variables {α β γ δ : Type*}

section ne_imp

variable {r : α → α → Prop}

lemma is_refl.reflexive [is_refl α r] : reflexive r :=
λ x, is_refl.refl x

/-- To show a reflexive relation `r : α → α → Prop` holds over `x y : α`,
it suffices to show it holds when `x ≠ y`. -/
lemma reflexive.rel_of_ne_imp (h : reflexive r) {x y : α} (hr : x ≠ y → r x y) : r x y :=
begin
  by_cases hxy : x = y,
  { exact hxy ▸ h x },
  { exact hr hxy }
end

/-- If a reflexive relation `r : α → α → Prop` holds over `x y : α`,
then it holds whether or not `x ≠ y`. -/
lemma reflexive.ne_imp_iff (h : reflexive r) {x y : α} :
  (x ≠ y → r x y) ↔ r x y :=
⟨h.rel_of_ne_imp, λ hr _, hr⟩

/-- If a reflexive relation `r : α → α → Prop` holds over `x y : α`,
then it holds whether or not `x ≠ y`. Unlike `reflexive.ne_imp_iff`, this uses `[is_refl α r]`. -/
lemma reflexive_ne_imp_iff [is_refl α r] {x y : α} :
  (x ≠ y → r x y) ↔ r x y :=
is_refl.reflexive.ne_imp_iff

protected lemma symmetric.iff (H : symmetric r) (x y : α) : r x y ↔ r y x := ⟨λ h, H h, λ h, H h⟩

lemma symmetric.flip_eq (h : symmetric r) : flip r = r := funext₂ $ λ _ _, propext $ h.iff _ _
lemma symmetric.swap_eq : symmetric r → swap r = r := symmetric.flip_eq

lemma flip_eq_iff : flip r = r ↔ symmetric r := ⟨λ h x y, (congr_fun₂ h _ _).mp, symmetric.flip_eq⟩
lemma swap_eq_iff : swap r = r ↔ symmetric r := flip_eq_iff

end ne_imp

section comap

variables {r : β → β → Prop}

lemma reflexive.comap (h : reflexive r) (f : α → β) : reflexive (r on f) :=
λ a, h (f a)

lemma symmetric.comap (h : symmetric r) (f : α → β) : symmetric (r on f) :=
λ a b hab, h hab

lemma transitive.comap (h : transitive r) (f : α → β) : transitive (r on f) :=
λ a b c hab hbc, h hab hbc

lemma equivalence.comap (h : equivalence r) (f : α → β) : equivalence (r on f) :=
⟨h.1.comap f, h.2.1.comap f, h.2.2.comap f⟩

end comap

namespace relation

section comp
variables {r : α → β → Prop} {p : β → γ → Prop} {q : γ → δ → Prop}

/--
The composition of two relations, yielding a new relation.  The result
relates a term of `α` and a term of `γ` if there is an intermediate
term of `β` related to both.
-/
def comp (r : α → β → Prop) (p : β → γ → Prop) (a : α) (c : γ) : Prop := ∃ b, r a b ∧ p b c

local infixr ` ∘r ` : 80 := relation.comp

lemma comp_eq : r ∘r (=) = r :=
funext $ λ a, funext $ λ b, propext $ iff.intro
  (λ ⟨c, h, eq⟩, eq ▸ h)
  (λ h, ⟨b, h, rfl⟩)

lemma eq_comp : (=) ∘r r = r :=
funext $ λ a, funext $ λ b, propext $ iff.intro
  (λ ⟨c, eq, h⟩, eq.symm ▸ h)
  (λ h, ⟨a, rfl, h⟩)

lemma iff_comp {r : Prop → α → Prop} : (↔) ∘r r = r :=
have (↔) = (=), by funext a b; exact iff_eq_eq,
by rw [this, eq_comp]

lemma comp_iff {r : α → Prop → Prop} : r ∘r (↔) = r :=
have (↔) = (=), by funext a b; exact iff_eq_eq,
by rw [this, comp_eq]

lemma comp_assoc : (r ∘r p) ∘r q = r ∘r p ∘r q :=
begin
  funext a d, apply propext,
  split,
  exact λ ⟨c, ⟨b, hab, hbc⟩, hcd⟩, ⟨b, hab, c, hbc, hcd⟩,
  exact λ ⟨b, hab, c, hbc, hcd⟩, ⟨c, ⟨b, hab, hbc⟩, hcd⟩
end

lemma flip_comp : flip (r ∘r p) = (flip p) ∘r (flip r) :=
begin
  funext c a, apply propext,
  split,
  exact λ ⟨b, hab, hbc⟩, ⟨b, hbc, hab⟩,
  exact λ ⟨b, hbc, hab⟩, ⟨b, hab, hbc⟩
end

end comp

section fibration

variables (rα : α → α → Prop) (rβ : β → β → Prop) (f : α → β)

/-- A function `f : α → β` is a fibration between the relation `rα` and `rβ` if for all
  `a : α` and `b : β`, whenever `b : β` and `f a` are related by `rβ`, `b` is the image
  of some `a' : α` under `f`, and `a'` and `a` are related by `rα`. -/
def fibration := ∀ ⦃a b⦄, rβ b (f a) → ∃ a', rα a' a ∧ f a' = b

variables {rα rβ}

/-- If `f : α → β` is a fibration between relations `rα` and `rβ`, and `a : α` is
  accessible under `rα`, then `f a` is accessible under `rβ`. -/
lemma _root_.acc.of_fibration (fib : fibration rα rβ f) {a} (ha : acc rα a) : acc rβ (f a) :=
begin
  induction ha with a ha ih,
  refine acc.intro (f a) (λ b hr, _),
  obtain ⟨a', hr', rfl⟩ := fib hr,
  exact ih a' hr',
end

lemma _root_.acc.of_downward_closed (dc : ∀ {a b}, rβ b (f a) → ∃ c, f c = b)
  (a : α) (ha : acc (inv_image rβ f) a) : acc rβ (f a) :=
ha.of_fibration f (λ a b h, let ⟨a', he⟩ := dc h in ⟨a', he.substr h, he⟩)

end fibration

/--
The map of a relation `r` through a pair of functions pushes the
relation to the codomains of the functions.  The resulting relation is
defined by having pairs of terms related if they have preimages
related by `r`.
-/
protected def map (r : α → β → Prop) (f : α → γ) (g : β → δ) : γ → δ → Prop :=
λ c d, ∃ a b, r a b ∧ f a = c ∧ g b = d

variables {r : α → α → Prop} {a b c d : α}

/-- `refl_trans_gen r`: reflexive transitive closure of `r` -/
@[mk_iff relation.refl_trans_gen.cases_tail_iff]
inductive refl_trans_gen (r : α → α → Prop) (a : α) : α → Prop
| refl : refl_trans_gen a
| tail {b c} : refl_trans_gen b → r b c → refl_trans_gen c

attribute [refl] refl_trans_gen.refl

/-- `refl_gen r`: reflexive closure of `r` -/
@[mk_iff] inductive refl_gen (r : α → α → Prop) (a : α) : α → Prop
| refl : refl_gen a
| single {b} : r a b → refl_gen b

/-- `trans_gen r`: transitive closure of `r` -/
@[mk_iff] inductive trans_gen (r : α → α → Prop) (a : α) : α → Prop
| single {b} : r a b → trans_gen b
| tail {b c} : trans_gen b → r b c → trans_gen c

attribute [refl] refl_gen.refl

namespace refl_gen

lemma to_refl_trans_gen : ∀ {a b}, refl_gen r a b → refl_trans_gen r a b
| a _ refl := by refl
| a b (single h) := refl_trans_gen.tail refl_trans_gen.refl h

instance : is_refl α (refl_gen r) :=
⟨@refl α r⟩

end refl_gen

namespace refl_trans_gen

@[trans]
lemma trans (hab : refl_trans_gen r a b) (hbc : refl_trans_gen r b c) : refl_trans_gen r a c :=
begin
  induction hbc,
  case refl_trans_gen.refl { assumption },
  case refl_trans_gen.tail : c d hbc hcd hac { exact hac.tail hcd }
end

lemma single (hab : r a b) : refl_trans_gen r a b :=
refl.tail hab

lemma head (hab : r a b) (hbc : refl_trans_gen r b c) : refl_trans_gen r a c :=
begin
  induction hbc,
  case refl_trans_gen.refl { exact refl.tail hab },
  case refl_trans_gen.tail : c d hbc hcd hac { exact hac.tail hcd }
end

lemma symmetric (h : symmetric r) : symmetric (refl_trans_gen r) :=
begin
  intros x y h,
  induction h with z w a b c,
  { refl },
  { apply relation.refl_trans_gen.head (h b) c }
end

lemma cases_tail : refl_trans_gen r a b → b = a ∨ (∃ c, refl_trans_gen r a c ∧ r c b) :=
(cases_tail_iff r a b).1

@[elab_as_eliminator]
lemma head_induction_on
  {P : ∀ (a:α), refl_trans_gen r a b → Prop}
  {a : α} (h : refl_trans_gen r a b)
  (refl : P b refl)
  (head : ∀ {a c} (h' : r a c) (h : refl_trans_gen r c b), P c h → P a (h.head h')) :
  P a h :=
begin
  induction h generalizing P,
  case refl_trans_gen.refl { exact refl },
  case refl_trans_gen.tail : b c hab hbc ih
  { apply ih,
    show P b _, from head hbc _ refl,
    show ∀ a a', r a a' → refl_trans_gen r a' b → P a' _ → P a _,
      from λ a a' hab hbc, head hab _ }
end

@[elab_as_eliminator]
lemma trans_induction_on
  {P : ∀ {a b : α}, refl_trans_gen r a b → Prop}
  {a b : α} (h : refl_trans_gen r a b)
  (ih₁ : ∀ a, @P a a refl)
  (ih₂ : ∀ {a b} (h : r a b), P (single h))
  (ih₃ : ∀ {a b c} (h₁ : refl_trans_gen r a b) (h₂ : refl_trans_gen r b c),
    P h₁ → P h₂ → P (h₁.trans h₂)) :
  P h :=
begin
  induction h,
  case refl_trans_gen.refl { exact ih₁ a },
  case refl_trans_gen.tail : b c hab hbc ih { exact ih₃ hab (single hbc) ih (ih₂ hbc) }
end

lemma cases_head (h : refl_trans_gen r a b) : a = b ∨ (∃ c, r a c ∧ refl_trans_gen r c b) :=
begin
  induction h using relation.refl_trans_gen.head_induction_on,
  { left, refl },
  { right, existsi _, split; assumption }
end

lemma cases_head_iff : refl_trans_gen r a b ↔ a = b ∨ (∃ c, r a c ∧ refl_trans_gen r c b) :=
begin
  use cases_head,
  rintro (rfl | ⟨c, hac, hcb⟩),
  { refl },
  { exact head hac hcb }
end

lemma total_of_right_unique (U : relator.right_unique r)
  (ab : refl_trans_gen r a b) (ac : refl_trans_gen r a c) :
  refl_trans_gen r b c ∨ refl_trans_gen r c b :=
begin
  induction ab with b d ab bd IH,
  { exact or.inl ac },
  { rcases IH with IH | IH,
    { rcases cases_head IH with rfl | ⟨e, be, ec⟩,
      { exact or.inr (single bd) },
      { cases U bd be, exact or.inl ec } },
    { exact or.inr (IH.tail bd) } }
end

end refl_trans_gen

namespace trans_gen

lemma to_refl {a b} (h : trans_gen r a b) : refl_trans_gen r a b :=
begin
  induction h with b h b c _ bc ab,
  exact refl_trans_gen.single h,
  exact refl_trans_gen.tail ab bc
end

@[trans] lemma trans_left (hab : trans_gen r a b) (hbc : refl_trans_gen r b c) : trans_gen r a c :=
begin
  induction hbc,
  case refl_trans_gen.refl : { assumption },
  case refl_trans_gen.tail : c d hbc hcd hac { exact hac.tail hcd }
end

@[trans] lemma trans (hab : trans_gen r a b) (hbc : trans_gen r b c) : trans_gen r a c :=
trans_left hab hbc.to_refl

lemma head' (hab : r a b) (hbc : refl_trans_gen r b c) : trans_gen r a c :=
trans_left (single hab) hbc

lemma tail' (hab : refl_trans_gen r a b) (hbc : r b c) : trans_gen r a c :=
begin
  induction hab generalizing c,
  case refl_trans_gen.refl : c hac { exact single hac },
  case refl_trans_gen.tail : d b hab hdb IH { exact tail (IH hdb) hbc }
end

lemma head (hab : r a b) (hbc : trans_gen r b c) : trans_gen r a c :=
head' hab hbc.to_refl

@[elab_as_eliminator]
lemma head_induction_on
  {P : ∀ (a:α), trans_gen r a b → Prop}
  {a : α} (h : trans_gen r a b)
  (base : ∀ {a} (h : r a b), P a (single h))
  (ih : ∀ {a c} (h' : r a c) (h : trans_gen r c b), P c h → P a (h.head h')) :
  P a h :=
begin
  induction h generalizing P,
  case single : a h { exact base h },
  case tail : b c hab hbc h_ih
  { apply h_ih,
    show ∀ a, r a b → P a _, from λ a h, ih h (single hbc) (base hbc),
    show ∀ a a', r a a' → trans_gen r a' b → P a' _ → P a _, from λ a a' hab hbc, ih hab _ }
end

@[elab_as_eliminator]
lemma trans_induction_on
  {P : ∀ {a b : α}, trans_gen r a b → Prop}
  {a b : α} (h : trans_gen r a b)
  (base : ∀ {a b} (h : r a b), P (single h))
  (ih : ∀ {a b c} (h₁ : trans_gen r a b) (h₂ : trans_gen r b c), P h₁ → P h₂ → P (h₁.trans h₂)) :
  P h :=
begin
  induction h,
  case single : a h { exact base h },
  case tail : b c hab hbc h_ih { exact ih hab (single hbc) h_ih (base hbc) }
end

@[trans] lemma trans_right (hab : refl_trans_gen r a b) (hbc : trans_gen r b c) : trans_gen r a c :=
begin
  induction hbc,
  case trans_gen.single : c hbc { exact tail' hab hbc },
  case trans_gen.tail : c d hbc hcd hac { exact hac.tail hcd }
end

lemma tail'_iff : trans_gen r a c ↔ ∃ b, refl_trans_gen r a b ∧ r b c :=
begin
  refine ⟨λ h, _, λ ⟨b, hab, hbc⟩, tail' hab hbc⟩,
  cases h with _ hac b _ hab hbc,
  { exact ⟨_, by refl, hac⟩ },
  { exact ⟨_, hab.to_refl, hbc⟩ }
end

lemma head'_iff : trans_gen r a c ↔ ∃ b, r a b ∧ refl_trans_gen r b c :=
begin
  refine ⟨λ h, _, λ ⟨b, hab, hbc⟩, head' hab hbc⟩,
  induction h,
  case trans_gen.single : c hac { exact ⟨_, hac, by refl⟩ },
  case trans_gen.tail : b c hab hbc IH
  { rcases IH with ⟨d, had, hdb⟩, exact ⟨_, had, hdb.tail hbc⟩ }
end

end trans_gen

lemma _root_.acc.trans_gen (h : acc r a) : acc (trans_gen r) a :=
begin
  induction h with x _ H,
  refine acc.intro x (λ y hy, _),
  cases hy with _ hyx z _ hyz hzx,
  exacts [H y hyx, (H z hzx).inv hyz],
end

lemma _root_.acc_trans_gen_iff : acc (trans_gen r) a ↔ acc r a :=
⟨subrelation.accessible (λ _ _, trans_gen.single), acc.trans_gen⟩

lemma _root_.well_founded.trans_gen (h : well_founded r) : well_founded (trans_gen r) :=
⟨λ a, (h.apply a).trans_gen⟩

section trans_gen

lemma trans_gen_eq_self (trans : transitive r) :
  trans_gen r = r :=
funext $ λ a, funext $ λ b, propext $
⟨λ h, begin
  induction h,
  case trans_gen.single : c hc { exact hc },
  case trans_gen.tail : c d hac hcd hac { exact trans hac hcd }
end,
trans_gen.single⟩

lemma transitive_trans_gen : transitive (trans_gen r) :=
λ a b c, trans_gen.trans

instance : is_trans α (trans_gen r) :=
⟨@trans_gen.trans α r⟩

lemma trans_gen_idem :
  trans_gen (trans_gen r) = trans_gen r :=
trans_gen_eq_self transitive_trans_gen

lemma trans_gen.lift {p : β → β → Prop} {a b : α} (f : α → β)
  (h : ∀ a b, r a b → p (f a) (f b)) (hab : trans_gen r a b) : trans_gen p (f a) (f b) :=
begin
  induction hab,
  case trans_gen.single : c hac { exact trans_gen.single (h a c hac) },
  case trans_gen.tail : c d hac hcd hac { exact trans_gen.tail hac (h c d hcd) }
end

lemma trans_gen.lift' {p : β → β → Prop} {a b : α} (f : α → β)
  (h : ∀ a b, r a b → trans_gen p (f a) (f b))
  (hab : trans_gen r a b) : trans_gen p (f a) (f b) :=
by simpa [trans_gen_idem] using hab.lift f h

lemma trans_gen.closed {p : α → α → Prop} :
  (∀ a b, r a b → trans_gen p a b) → trans_gen r a b → trans_gen p a b :=
trans_gen.lift' id

lemma trans_gen.mono {p : α → α → Prop} :
  (∀ a b, r a b → p a b) → trans_gen r a b → trans_gen p a b :=
trans_gen.lift id

lemma trans_gen.swap (h : trans_gen r b a) : trans_gen (swap r) a b :=
by { induction h with b h b c hab hbc ih, { exact trans_gen.single h }, exact ih.head hbc }

lemma trans_gen_swap : trans_gen (swap r) a b ↔ trans_gen r b a :=
⟨trans_gen.swap, trans_gen.swap⟩

end trans_gen

section refl_trans_gen
open refl_trans_gen

lemma refl_trans_gen_iff_eq (h : ∀ b, ¬ r a b) : refl_trans_gen r a b ↔ b = a :=
by rw [cases_head_iff]; simp [h, eq_comm]

lemma refl_trans_gen_iff_eq_or_trans_gen :
  refl_trans_gen r a b ↔ b = a ∨ trans_gen r a b :=
begin
  refine ⟨λ h, _, λ h, _⟩,
  { cases h with c _ hac hcb,
    { exact or.inl rfl },
    { exact or.inr (trans_gen.tail' hac hcb) } },
  { rcases h with rfl | h, {refl}, {exact h.to_refl} }
end

lemma refl_trans_gen.lift {p : β → β → Prop} {a b : α} (f : α → β)
  (h : ∀ a b, r a b → p (f a) (f b)) (hab : refl_trans_gen r a b) : refl_trans_gen p (f a) (f b) :=
refl_trans_gen.trans_induction_on hab (λ a, refl)
  (λ a b, refl_trans_gen.single ∘ h _ _) (λ a b c _ _, trans)

lemma refl_trans_gen.mono {p : α → α → Prop} :
  (∀ a b, r a b → p a b) → refl_trans_gen r a b → refl_trans_gen p a b :=
refl_trans_gen.lift id

lemma refl_trans_gen_eq_self (refl : reflexive r) (trans : transitive r) :
  refl_trans_gen r = r :=
funext $ λ a, funext $ λ b, propext $
⟨λ h, begin
  induction h with b c h₁ h₂ IH, {apply refl},
  exact trans IH h₂,
end, single⟩

lemma reflexive_refl_trans_gen : reflexive (refl_trans_gen r) :=
λ a, refl

lemma transitive_refl_trans_gen : transitive (refl_trans_gen r) :=
λ a b c, trans

instance : is_refl α (refl_trans_gen r) :=
⟨@refl_trans_gen.refl α r⟩

instance : is_trans α (refl_trans_gen r) :=
⟨@refl_trans_gen.trans α r⟩

lemma refl_trans_gen_idem :
  refl_trans_gen (refl_trans_gen r) = refl_trans_gen r :=
refl_trans_gen_eq_self reflexive_refl_trans_gen transitive_refl_trans_gen

lemma refl_trans_gen.lift' {p : β → β → Prop} {a b : α} (f : α → β)
  (h : ∀ a b, r a b → refl_trans_gen p (f a) (f b))
  (hab : refl_trans_gen r a b) : refl_trans_gen p (f a) (f b) :=
by simpa [refl_trans_gen_idem] using hab.lift f h

lemma refl_trans_gen_closed {p : α → α → Prop} :
  (∀ a b, r a b → refl_trans_gen p a b) → refl_trans_gen r a b → refl_trans_gen p a b :=
refl_trans_gen.lift' id

lemma refl_trans_gen.swap (h : refl_trans_gen r b a) : refl_trans_gen (swap r) a b :=
by { induction h with b c hab hbc ih, { refl }, exact ih.head hbc }

lemma refl_trans_gen_swap : refl_trans_gen (swap r) a b ↔ refl_trans_gen r b a :=
⟨refl_trans_gen.swap, refl_trans_gen.swap⟩

end refl_trans_gen

/--
The join of a relation on a single type is a new relation for which
pairs of terms are related if there is a third term they are both
related to.  For example, if `r` is a relation representing rewrites
in a term rewriting system, then *confluence* is the property that if
`a` rewrites to both `b` and `c`, then `join r` relates `b` and `c`
(see `relation.church_rosser`).
-/
def join (r : α → α → Prop) : α → α → Prop := λ a b, ∃ c, r a c ∧ r b c

section join
open refl_trans_gen refl_gen

/-- A sufficient condition for the Church-Rosser property. -/
lemma church_rosser
  (h : ∀ a b c, r a b → r a c → ∃ d, refl_gen r b d ∧ refl_trans_gen r c d)
  (hab : refl_trans_gen r a b) (hac : refl_trans_gen r a c) : join (refl_trans_gen r) b c :=
begin
  induction hab,
  case refl_trans_gen.refl { exact ⟨c, hac, refl⟩ },
  case refl_trans_gen.tail : d e had hde ih
  { clear hac had a,
    rcases ih with ⟨b, hdb, hcb⟩,
    have : ∃ a, refl_trans_gen r e a ∧ refl_gen r b a,
    { clear hcb, induction hdb,
      case refl_trans_gen.refl { exact ⟨e, refl, refl_gen.single hde⟩ },
      case refl_trans_gen.tail : f b hdf hfb ih
      { rcases ih with ⟨a, hea, hfa⟩,
        cases hfa with _ hfa,
        { exact ⟨b, hea.tail hfb, refl_gen.refl⟩ },
        { rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩,
          exact ⟨c, hea.trans hac, hbc⟩ } } },
    rcases this with ⟨a, hea, hba⟩, cases hba with _ hba,
    { exact ⟨b, hea, hcb⟩ },
    { exact ⟨a, hea, hcb.tail hba⟩ } }
end

lemma join_of_single (h : reflexive r) (hab : r a b) : join r a b :=
⟨b, hab, h b⟩

lemma symmetric_join : symmetric (join r) :=
λ a b ⟨c, hac, hcb⟩, ⟨c, hcb, hac⟩

lemma reflexive_join (h : reflexive r) : reflexive (join r) :=
λ a, ⟨a, h a, h a⟩

lemma transitive_join (ht : transitive r) (h : ∀ a b c, r a b → r a c → join r b c) :
  transitive (join r) :=
λ a b c ⟨x, hax, hbx⟩ ⟨y, hby, hcy⟩,
let ⟨z, hxz, hyz⟩ := h b x y hbx hby in
⟨z, ht hax hxz, ht hcy hyz⟩

lemma equivalence_join (hr : reflexive r) (ht : transitive r)
  (h : ∀ a b c, r a b → r a c → join r b c) :
  equivalence (join r) :=
⟨reflexive_join hr, symmetric_join, transitive_join ht h⟩

lemma equivalence_join_refl_trans_gen
  (h : ∀ a b c, r a b → r a c → ∃ d, refl_gen r b d ∧ refl_trans_gen r c d) :
  equivalence (join (refl_trans_gen r)) :=
equivalence_join reflexive_refl_trans_gen transitive_refl_trans_gen (λ a b c, church_rosser h)

lemma join_of_equivalence {r' : α → α → Prop} (hr : equivalence r)
  (h : ∀ a b, r' a b → r a b) : join r' a b → r a b
| ⟨c, hac, hbc⟩ := hr.2.2 (h _ _ hac) (hr.2.1 $ h _ _ hbc)

lemma refl_trans_gen_of_transitive_reflexive {r' : α → α → Prop} (hr : reflexive r)
  (ht : transitive r) (h : ∀ a b, r' a b → r a b) (h' : refl_trans_gen r' a b) :
  r a b :=
begin
  induction h' with b c hab hbc ih,
  { exact hr _ },
  { exact ht ih (h _ _ hbc) }
end

lemma refl_trans_gen_of_equivalence {r' : α → α → Prop} (hr : equivalence r) :
  (∀ a b, r' a b → r a b) → refl_trans_gen r' a b → r a b :=
refl_trans_gen_of_transitive_reflexive hr.1 hr.2.2

end join

end relation

section eqv_gen

variables {r : α → α → Prop} {a b : α}

lemma equivalence.eqv_gen_iff (h : equivalence r) : eqv_gen r a b ↔ r a b :=
iff.intro
  begin
    intro h,
    induction h,
    case eqv_gen.rel { assumption },
    case eqv_gen.refl { exact h.1 _ },
    case eqv_gen.symm { apply h.2.1, assumption },
    case eqv_gen.trans : a b c _ _ hab hbc { exact h.2.2 hab hbc }
  end
  (eqv_gen.rel a b)

lemma equivalence.eqv_gen_eq (h : equivalence r) : eqv_gen r = r :=
funext $ λ _, funext $ λ _, propext $ h.eqv_gen_iff

lemma eqv_gen.mono {r p : α → α → Prop}
  (hrp : ∀ a b, r a b → p a b) (h : eqv_gen r a b) : eqv_gen p a b :=
begin
  induction h,
  case eqv_gen.rel : a b h { exact eqv_gen.rel _ _ (hrp _ _ h) },
  case eqv_gen.refl : { exact eqv_gen.refl _ },
  case eqv_gen.symm : a b h ih { exact eqv_gen.symm _ _ ih },
  case eqv_gen.trans : a b c ih1 ih2 hab hbc { exact eqv_gen.trans _ _ _ hab hbc }
end

end eqv_gen

author: leanprover-community

repo: mathlib


text:
/-
Copyright (c) 2021 Yaël Dillies, Bhavik Mehta. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies, Bhavik Mehta
-/
import combinatorics.simplicial_complex.simplex
-- import data.nat.parity

open_locale classical affine big_operators
open set

namespace affine

/--
A simplicial complex in `R^m`.
TODO: generalise to normed affine spaces `E`, so this is `simplicial_complex E`.
-/
@[ext] structure simplicial_complex (E : Type*) [normed_group E] [normed_space ℝ E] :=
(faces : set (finset E))
(indep : ∀ {X}, X ∈ faces → affine_independent ℝ (λ p, p : (X : set E) → E))
(down_closed : ∀ {X Y}, X ∈ faces → Y ⊆ X → Y ∈ faces)
(disjoint : ∀ {X Y}, X ∈ faces → Y ∈ faces →
  convex_hull ↑X ∩ convex_hull ↑Y ⊆ convex_hull (X ∩ Y : set E))

variables {m n : ℕ} {E : Type*} [normed_group E] [normed_space ℝ E] {S : simplicial_complex E}
  {x y : E} {X Y : finset E} {A : set (finset E)}
--local notation `E` := E

/--
A constructor for simplicial complexes by specifying a surcomplex whose set of faces is
downward closed.
-/
@[simp] def simplicial_complex.of_surcomplex
  (faces : set (finset E)) (subset_surcomplex : faces ⊆ S.faces)
  (down_closed : ∀ {X Y}, X ∈ faces → Y ⊆ X → Y ∈ faces) :
  simplicial_complex E :=
{ faces := faces,
  indep := λ X hX, S.indep (subset_surcomplex hX),
  down_closed := λ X Y hX hYX, down_closed hX hYX,
  disjoint := λ X Y hX hY, S.disjoint (subset_surcomplex hX) (subset_surcomplex hY) }

/--
A constructor for simplicial complexes by specifying a set of faces to close downward.
-/
@[simp] def simplicial_complex.of_set_closure
  (indep : ∀ {X}, X ∈ A → affine_independent ℝ (λ p, p : (X : set E) → E))
  (disjoint : ∀ {X Y}, X ∈ A → Y ∈ A →
    convex_hull ↑X ∩ convex_hull ↑Y ⊆ convex_hull (X ∩ Y : set E)) :
  simplicial_complex E :=
{ faces := {X | ∃ Y, Y ∈ A ∧ X ⊆ Y},
  indep := λ X ⟨Y, hY, hXY⟩, affine_independent_of_subset_affine_independent (indep hY) hXY,
  down_closed := λ X Y ⟨Z, hZ, hXZ⟩ hYX, ⟨Z, hZ, subset.trans hYX hXZ⟩,
  disjoint :=
  begin
    rintro W X ⟨Y, hY, hWY⟩ ⟨Z, hZ, hXZ⟩ x ⟨hxW, hxX⟩,
    have hxYZ : x ∈ convex_hull (Y ∩ Z : set E) :=
      disjoint hY hZ ⟨convex_hull_mono hWY hxW, convex_hull_mono hXZ hxX⟩,
    have hxWZ : x ∈ convex_hull (W ∩ Z : set E),
    { have := disjoint_convex_hull_of_subsets (indep hY) hWY (finset.inter_subset_left Y Z),
      norm_cast at this hxYZ,
      exact_mod_cast convex_hull_mono
        (finset.inter_subset_inter_left (finset.inter_subset_right Y Z)) (this ⟨hxW, hxYZ⟩), },
    have hxYX : x ∈ convex_hull (Y ∩ X : set E),
    { have := disjoint_convex_hull_of_subsets (indep hZ) (finset.inter_subset_right Y Z) hXZ,
      norm_cast at this hxYZ,
      exact_mod_cast convex_hull_mono
        (finset.inter_subset_inter_right (finset.inter_subset_left Y Z)) (this ⟨hxYZ, hxX⟩), },
    norm_cast at hxWZ hxYX,
    have hxWX := disjoint_convex_hull_of_subsets (indep hY)
      (subset.trans (finset.inter_subset_inter_right hWY) (finset.inter_subset_left Y Z))
      (finset.inter_subset_left Y X) ⟨hxWZ, hxYX⟩,
    norm_cast at hxWX,
    exact_mod_cast convex_hull_mono (subset.trans
      (finset.inter_subset_inter_right (finset.inter_subset_left W Z))
      (finset.inter_subset_inter_left (finset.inter_subset_right Y X))) hxWX,
  end}

/--
A constructor for simplicial complexes by specifying a face to close downward.
-/
@[simp] def simplicial_complex.of_simplex
  (indep : affine_independent ℝ (λ p, p : (X : set E) → E)) :
  simplicial_complex E :=
simplicial_complex.of_set_closure
  begin rintro Y (hY : Y = X), rw hY, exact indep end
  begin rintro Y Z (hY : Y = X) (hZ : Z = X), rw [hY, hZ, inter_self _, inter_self _],
    exact subset.refl _ end

lemma mem_simplex_complex_iff
  (hX : affine_independent ℝ (λ p, p : (X : set E) → E)) :
  Y ∈ (simplicial_complex.of_simplex hX).faces ↔ Y ⊆ X :=
begin
  split,
  { rintro ⟨Z, (hZ : Z = X), hYX⟩,
    rw ← hZ,
    exact hYX },
  { rintro hYX,
    exact ⟨X, rfl, hYX⟩ }
end

/--
The empty simplicial complex is made up of only the empty simplex
-/
def empty_simplicial_complex (E : Type*) [normed_group E] [normed_space ℝ E] :
  simplicial_complex E :=
{ faces := {∅},
  indep :=
  begin
    rintro X (rfl : _ = _),
    apply affine_independent_of_subsingleton ℝ _,
    simp,
  end,
  down_closed := λ X Y hX, hX.symm ▸ finset.subset_empty.1,
  disjoint :=
  begin
    rintro X _ (rfl : X = ∅) (rfl : Y = ∅),
    simp,
  end, }

lemma empty_mem_faces_of_nonempty :
  (S.faces).nonempty → ∅ ∈ S.faces :=
λ ⟨X, hX⟩, S.down_closed hX (empty_subset X)

/--
The underlying space of a simplicial complex.
-/
def simplicial_complex.space (S : simplicial_complex E) :
  set E :=
⋃ X ∈ S.faces, convex_hull (X : set E)

lemma mem_space_iff :
  x ∈ S.space ↔ ∃ X ∈ S.faces, x ∈ convex_hull (X : set E) :=
begin
  unfold simplicial_complex.space,
  rw mem_bUnion_iff,
end

lemma empty_space_of_empty_simplicial_complex :
  (empty_simplicial_complex E).space = ∅ :=
begin
  unfold empty_simplicial_complex simplicial_complex.space,
  simp,
end

lemma convex_hull_face_subset_space (hX : X ∈ S.faces) :
  convex_hull ↑X ⊆ S.space :=
λ x hx, mem_bUnion hX hx

lemma face_subset_space (hX : X ∈ S.faces) :
  (X : set E) ⊆ S.space :=
set.subset.trans (subset_convex_hull _) (convex_hull_face_subset_space hX)

def simplicial_complex.points (S : simplicial_complex E) :
  set E :=
⋃ k ∈ S.faces, (k : set E)

lemma points_subset_space :
  S.points ⊆ S.space :=
bUnion_subset_bUnion_right (λ x hx, subset_convex_hull x)

--noncomputable def simplicial_complex.dim (S : simplicial_complex E) :
--  ℕ :=

-- Dumb bug in mathlib, see
--https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/R.5Em.20is.20finite.20dimensional.20over.20R/near/231748016
--instance {m : ℕ} : finite_dimensional ℝ E := sorry

--Refinement of `size_bound`
lemma face_dimension_le_space_dimension [finite_dimensional ℝ E] (hX : X ∈ S.faces) :
  finset.card X ≤ finite_dimensional.finrank ℝ E + 1 :=
size_bound (S.indep hX)

def simplicial_complex.facets (S : simplicial_complex E) :
  set (finset E) :=
{X | X ∈ S.faces ∧ (∀ {Y}, Y ∈ S.faces → X ⊆ Y → X = Y)}

lemma facets_subset : S.facets ⊆ S.faces := λ X hX, hX.1

lemma not_facet_iff_subface : X ∈ S.faces → (X ∉ S.facets ↔ ∃ {Y}, Y ∈ S.faces ∧ X ⊂ Y) :=
begin
  rintro hX,
  split,
  { rintro (hX' : ¬(X ∈ S.faces ∧ (∀ {Y}, Y ∈ S.faces → X ⊆ Y → X = Y))),
    push_neg at hX',
    obtain ⟨Y, hY⟩ := hX' hX,
    exact ⟨Y, hY.1, ⟨hY.2.1, (λ hYX, hY.2.2 (finset.subset.antisymm hY.2.1 hYX))⟩⟩, },
  rintro ⟨Y, hY⟩ ⟨hX, hX'⟩,
  have := hX' hY.1 hY.2.1,
  rw this at hY,
  exact hY.2.2 (subset.refl Y),
end

lemma subfacet [finite_dimensional ℝ E] (hX : X ∈ S.faces) :
  ∃ {Y}, Y ∈ S.facets ∧ X ⊆ Y :=
begin
  have := id hX,
  revert this,
  apply finset.strong_downward_induction_on X,
  { rintro Y h hYcard hY,
    by_cases hYfacet : Y ∈ S.facets,
    { exact ⟨Y, hYfacet, finset.subset.refl _⟩, },
    obtain ⟨Z, hZ, hYZ⟩ := (not_facet_iff_subface hY).mp hYfacet,
    obtain ⟨W, hW⟩ := h (face_dimension_le_space_dimension hZ) hYZ hZ,
    exact ⟨W, hW.1, finset.subset.trans hYZ.1 hW.2⟩ },
  exact face_dimension_le_space_dimension hX,
end

lemma facets_empty (hS : S.faces = ∅) :
  S.facets = ∅ :=
begin
  rw [←subset_empty_iff, ←hS],
  exact facets_subset,
end

lemma facets_empty_iff_faces_empty [finite_dimensional ℝ E] :
  S.facets = ∅ ↔ S.faces = ∅ :=
begin
  classical,
  split,
  { intro h,
    by_contra h',
    rw [←ne.def, set.ne_empty_iff_nonempty] at h',
    obtain ⟨X, hX⟩ := h',
    obtain ⟨Y, hY, hZ⟩ := subfacet hX,
    rw h at hY,
    apply hY },
  exact facets_empty,
end

lemma facets_singleton (hS : S.faces = {X}) :
  S.facets = {X} :=
begin
  ext X,
  unfold simplicial_complex.facets,
  rw hS,
  simp,
  exact λ hX _, hX,
end

lemma facets_singleton_empty (hS : S.faces = {∅}) :
  S.facets = {∅} :=
facets_singleton hS

/--
The cells of a simplicial complex are its simplices whose dimension matches the one of the space.
-/
def simplicial_complex.cells (S : simplicial_complex E) :
  set (finset E) :=
{X | X ∈ S.faces ∧ X.card = finite_dimensional.finrank ℝ E + 1}

lemma cells_subset_facets [finite_dimensional ℝ E] :
  S.cells ⊆ S.facets :=
begin
  rintro X ⟨hX, hXcard⟩,
  by_contra,
  obtain ⟨Y, hY, hXY⟩ := (not_facet_iff_subface hX).mp h,
  have := finset.card_lt_card hXY,
  have := face_dimension_le_space_dimension hY,
  linarith,
end

/--
The subcells of a simplicial complex are its simplices whose cardinality matches the dimension of
the space. They are thus one smaller than cells.
-/
def simplicial_complex.subcells (S : simplicial_complex E) :
  set (finset E) :=
{X | X ∈ S.faces ∧ X.card = finite_dimensional.finrank ℝ E}

def simplicial_complex.vertices (S : simplicial_complex E) :
  set E :=
{x | {x} ∈ S.faces}

lemma mem_of_mem_convex_hull (hx : {x} ∈ S.faces) (hX : X ∈ S.faces)
  (hxX : x ∈ convex_hull (X : set E)) :
  x ∈ X :=
begin
  have h := S.disjoint hx hX ⟨by simp, hxX⟩,
  by_contra H,
  norm_cast at h,
  rw [finset.inter_comm, finset.disjoint_iff_inter_eq_empty.1 (finset.disjoint_singleton.2 H)] at h,
  simp at h,
  exact h,
end

lemma subset_of_convex_hull_subset_convex_hull (hX : X ∈ S.faces) (hY : Y ∈ S.faces)
  (hXY : convex_hull (X : set E) ⊆ convex_hull ↑Y) :
  X ⊆ Y :=
λ x hxX, mem_of_mem_convex_hull (S.down_closed hX (finset.singleton_subset_iff.2 hxX)) hY
  (hXY (subset_convex_hull ↑X hxX))

lemma disjoint_interiors (hX : X ∈ S.faces) (hY : Y ∈ S.faces) (hxX : x ∈ combi_interior X)
  (hxY : x ∈ combi_interior Y) :
  X = Y :=
begin
  by_contra,
  have hXY : X ∩ Y ⊂ X,
  { use finset.inter_subset_left X Y,
    intro H,
    exact hxY.2 (set.mem_bUnion ⟨subset.trans H (finset.inter_subset_right X Y), (λ H2,
      h (finset.subset.antisymm (subset.trans H (finset.inter_subset_right X Y)) H2))⟩ hxX.1) },
  refine hxX.2 (mem_bUnion hXY _),
  exact_mod_cast S.disjoint hX hY ⟨hxX.1, hxY.1⟩,
end

lemma disjoint_interiors_aux (hX : X ∈ S.faces) (hY : Y ∈ S.faces) (h : X ≠ Y) :
  disjoint (combi_interior X) (combi_interior Y) :=
λ x hx, h (disjoint_interiors hX hY hx.1 hx.2)

lemma eq_singleton_of_singleton_mem_combi_interior (hx : {x} ∈ S.faces) (hX : X ∈ S.faces)
  (hxX : x ∈ combi_interior X) :
    X = {x} :=
begin
  apply disjoint_interiors hX hx hxX,
  rw combi_interior_singleton,
  exact mem_singleton x,
end

lemma combi_interiors_cover :
  S.space = ⋃ X ∈ S.faces, combi_interior X :=
begin
  apply subset.antisymm _ _,
  { apply bUnion_subset,
    rintro X hX,
    rw simplex_combi_interiors_cover,
    exact Union_subset (λ Y, Union_subset (λ YX, subset_bUnion_of_mem (S.down_closed hX YX)))},
  { apply bUnion_subset,
    rintro Y hY,
    exact subset.trans (diff_subset _ _) (subset_bUnion_of_mem hY) }
end

/- The simplices interiors form a partition of the underlying space (except that they contain the
empty set) -/
lemma combi_interiors_partition (hx : x ∈ S.space) :
  ∃! X, X ∈ S.faces ∧ x ∈ combi_interior X :=
begin
  rw combi_interiors_cover at hx,
  simp only [set.mem_bUnion_iff] at hx,
  obtain ⟨X, hX, hxX⟩ := hx,
  exact ⟨X, ⟨⟨hX, hxX⟩, (λ Y ⟨hY, hxY⟩, disjoint_interiors hY hX hxY hxX)⟩⟩,
end

lemma mem_convex_hull_iff :
  x ∈ convex_hull (X : set E) ↔ ∃ Y ⊆ X, x ∈ combi_interior Y :=
begin
  simp [simplex_combi_interiors_cover],
end

lemma mem_combi_frontier_iff' :
  x ∈ combi_frontier X ↔ ∃ {Y}, Y ⊂ X ∧ x ∈ combi_interior Y :=
begin
  rw mem_combi_frontier_iff,
  split,
  {
    rintro ⟨Y, hYX, hxY⟩,
    --rw [simplex_combi_interiors_cover, mem_bUnion_iff] at hxY,
    --obtain ⟨Z, hZ⟩ := simplex_combi_interiors_cover
    sorry
  },
  { rintro ⟨Y, hYX, hxY⟩,
    exact ⟨Y, hYX, hxY.1⟩ }
end

lemma subset_of_combi_interior_inter_convex_hull_nonempty (hX : X ∈ S.faces) (hY : Y ∈ S.faces)
  (hXY : (combi_interior X ∩ convex_hull (Y : set E)).nonempty) :
  X ⊆ Y :=
begin
  obtain ⟨x, hxX, hxY⟩ := hXY,
  obtain ⟨Z, hZY, hxZ⟩ := mem_convex_hull_iff.1 hxY,
  rw disjoint_interiors hX (S.down_closed hY hZY) hxX hxZ,
  exact hZY,
end

lemma simplex_combi_interiors_split_interiors (hY : affine_independent ℝ (λ p, p : (Y : set E) → E))
  (hXY : convex_hull (X : set E) ⊆ convex_hull ↑Y) :
  ∃ Z ⊆ Y, combi_interior X ⊆ combi_interior Z :=
begin
  let S := simplicial_complex.of_simplex hY,
  --let F := Y.powerset.filter (λ W : finset E, (X : set E) ⊆ convex_hull W),
  sorry
  /-obtain ⟨Z, hZ, hZmin⟩ := finset.inf' _
  (begin
    use Y,
    simp only [true_and, finset.mem_powerset_self, finset.mem_filter],
    exact subset.trans (subset_convex_hull _) hXY,
  end : F.nonempty)
  begin
    rintro A B hA hB,
    simp at ⊢ hA hB,
    exact ⟨finset.subset.trans (finset.inter_subset_left _ _) hA.1,
      subset.trans (subset_inter hA.2 hB.2) (S.disjoint ((mem_simplex_complex_iff hY).2 hA.1)
      ((mem_simplex_complex_iff hY).2 hB.1))⟩
  end,
  simp at hZ,
  use [Z, hZ.1],
  rintro x hxX,
  use convex_hull_min hZ.2 (convex_convex_hull _) hxX.1,
  rintro hxZ,
  rw mem_combi_frontier_iff' at hxZ,
  obtain ⟨W, hWZ, hxW⟩ := hxZ,
  apply hWZ.2 (hZmin W _),
  simp,
  use [subset.trans hWZ.1 hZ.1],
  rw finset.convex_hull_eq _ at ⊢ hZ,
  obtain ⟨v, hvpos, hvsum, hvcenter⟩ := combi_interior_subset_positive_weighings hxX,
  obtain ⟨w, hwpos, hwsum, hwcenter⟩ := combi_interior_subset_positive_weighings hxW,
  let u : E → E → ℝ := λ a, if ha : a ∈ X then classical.some (hZ.2 ha) else (λ b, 0),
  have hupos : ∀ {a}, a ∈ X → ∀ (b : E), b ∈ Z → 0 < u a b,
  {
    rintro a ha,
    have := classical.some_spec (hZ.2 ha),
    sorry
  },
  have husum : ∀ {a}, a ∈ X → ∑ (b : E) in Z, u a b = 1,
  {
    sorry
  },
  have hucenter : ∀ {a}, a ∈ X → Z.center_mass (u a) id = a,
  {
    sorry
  },
  let t : E → ℝ := λ b, if hb : b ∈ Z then ∑ (a : E) in X, v a * u a b else 0,-/
  /-rintro y (hyX : y ∈ X),
  obtain ⟨v, hvpos, hvsum, hvcenter⟩ := combi_interior_subset_positive_weighings hxX,
  obtain ⟨w, hwpos, hwsum, hwcenter⟩ := combi_interior_subset_positive_weighings hxW,-/
  --rw mem_convex_hull,
  /-by_contra hXW,
  obtain ⟨y, hyX, hyW⟩ := not_subset.1 hXW,-/
  /-apply hxX.2,
  rw mem_combi_frontier_iff at ⊢,
  use [X.filter (λ w : E, w ∈ convex_hull (W : set E)), finset.filter_subset _ _],
  {
    rintro hXW,
    apply hWZ.2 (hZmin W _),
    simp,
    use [subset.trans hWZ.1 hZ.1],
    rintro y (hyX : y ∈ X),
    have := hXW hyX,
    simp at this,
    exact this.2,
  },
  {
    simp,
    apply convex_hull_mono (subset_inter (subset.refl _) _) hxX.1,
    by_contra hXW,
    rw not_subset at hXW,
    /-suffices hXW : ↑X ⊆ convex_hull ↑W,
    {
      apply convex_hull_mono (subset_inter (subset.refl _) hXW) hxX.1,
    },-/
    sorry
  }-/
end

end affine

author: mmasdeu

repo: brouwerfixedpoint


text:
/-
Copyright (c) 2018 Simon Hudon. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Simon Hudon
-/
import category_theory.category.basic

/-!
# The Kleisli construction on the Type category

Define the Kleisli category for (control) monads.
`category_theory/monad/kleisli` defines the general version for a monad on `C`, and demonstrates
the equivalence between the two.

## TODO

Generalise this to work with category_theory.monad
-/

universes u v

namespace category_theory

/-- The Kleisli category on the (type-)monad `m`. Note that the monad is not assumed to be lawful
yet. -/
@[nolint unused_arguments]
def Kleisli (m : Type u → Type v) := Type u

/-- Construct an object of the Kleisli category from a type. -/
def Kleisli.mk (m) (α : Type u) : Kleisli m := α

instance Kleisli.category_struct {m} [monad.{u v} m] : category_struct (Kleisli m) :=
{ hom := λ α β, α → m β,
  id := λ α x, pure x,
  comp := λ X Y Z f g, f >=> g }

instance Kleisli.category {m} [monad.{u v} m] [is_lawful_monad m] : category (Kleisli m) :=
by refine { id_comp' := _, comp_id' := _, assoc' := _ };
   intros; ext; unfold_projs; simp only [(>=>)] with functor_norm

@[simp] lemma Kleisli.id_def {m} [monad m] (α : Kleisli m) :
  𝟙 α = @pure m _ α := rfl

lemma Kleisli.comp_def {m} [monad m] (α β γ : Kleisli m)
  (xs : α ⟶ β) (ys : β ⟶ γ) (a : α) :
  (xs ≫ ys) a = xs a >>= ys := rfl

instance : inhabited (Kleisli id) := ⟨punit⟩
instance {α : Type u} [inhabited α] : inhabited (Kleisli.mk id α) := ⟨show α, from default⟩
end category_theory

author: Mel-TunaRoll

repo: Lean-Mordell-Weil-Mel-Branch


text:
#print option

namespace hidden

/-
Every function in Lean must be total.
That is, there has to be an answer for
*all* values of the argument type. This
constraint presents a problem in cases
where we want to represent *partial*
functions, i.e., functions that are
not defined for all values of their
argument types.

Suppose for example we want to represent
a partial function from bool to nat that
returns one if a given bool argument is
bool.tt and that is otherwise undefined.

We can represent this *partial* function
in Lean as a *total* function from bool
to the type "option nat", a simple sum
of products type, with two variants. The
"none" variant is interpreted as meaning
"no answer, the function is undefined at
the given argument value." By contrast,
the "some" variant boxes a value (a : α)
that holds the result for an argument on
which the function is defined.

Here's a polymorphic option type.
-/

inductive option (α : Type) : Type
| none : option
| some (a : α) : option

/-
EXERCISE: Represent the partial function
just described using the option type as
just explained. Write your definition in
a separate file, option_test.lean.
-/

end hidden

author: kevinsullivan


text:
/-
Copyright (c) 2021 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison
-/
import algebra.homology.image_to_kernel
import algebra.homology.homological_complex
import category_theory.graded_object

/-!
# The homology of a complex

Given `C : homological_complex V c`, we have `C.cycles i` and `C.boundaries i`,
both defined as subobjects of `C.X i`.

We show these are functorial with respect to chain maps,
as `C.cycles_map f i` and `C.boundaries_map f i`.

As a consequence we construct `homology_functor i : homological_complex V c ⥤ V`,
computing the `i`-th homology.
-/

universes v u

open category_theory category_theory.limits

variables {ι : Type*}
variables {V : Type u} [category.{v} V] [has_zero_morphisms V]
variables {c : complex_shape ι} (C : homological_complex V c)

open_locale classical zero_object
noncomputable theory

namespace homological_complex

variables [has_zero_object V]

section cycles
variables [has_kernels V]

/-- The cycles at index `i`, as a subobject. -/
abbreviation cycles (i : ι) : subobject (C.X i) :=
kernel_subobject (C.d_from i)

lemma cycles_eq_kernel_subobject {i j : ι} (r : c.rel i j) :
  C.cycles i = kernel_subobject (C.d i j) :=
C.kernel_from_eq_kernel r

/--
The underlying object of `C.cycles i` is isomorphic to `kernel (C.d i j)`,
for any `j` such that `rel i j`.
-/
def cycles_iso_kernel {i j : ι} (r : c.rel i j) :
  (C.cycles i : V) ≅ kernel (C.d i j) :=
subobject.iso_of_eq _ _ (C.cycles_eq_kernel_subobject r) ≪≫
  kernel_subobject_iso (C.d i j)

lemma cycles_eq_top {i} (h : c.next i = none) : C.cycles i = ⊤ :=
begin
  rw eq_top_iff,
  apply le_kernel_subobject,
  rw [C.d_from_eq_zero h, comp_zero],
end

end cycles

section boundaries
variables [has_images V]

/-- The boundaries at index `i`, as a subobject. -/
abbreviation boundaries (C : homological_complex V c) (j : ι) : subobject (C.X j) :=
image_subobject (C.d_to j)

lemma boundaries_eq_image_subobject [has_equalizers V] {i j : ι} (r : c.rel i j) :
  C.boundaries j = image_subobject (C.d i j) :=
C.image_to_eq_image r

/--
The underlying object of `C.boundaries j` is isomorphic to `image (C.d i j)`,
for any `i` such that `rel i j`.
-/
def boundaries_iso_image [has_equalizers V] {i j : ι} (r : c.rel i j) :
  (C.boundaries j : V) ≅ image (C.d i j) :=
subobject.iso_of_eq _ _ (C.boundaries_eq_image_subobject r) ≪≫
  image_subobject_iso (C.d i j)

lemma boundaries_eq_bot {j} (h : c.prev j = none) : C.boundaries j = ⊥ :=
begin
  rw eq_bot_iff,
  refine image_subobject_le _ 0 _,
  rw [C.d_to_eq_zero h, zero_comp],
end

end boundaries

section
variables [has_kernels V] [has_images V]

lemma boundaries_le_cycles (C : homological_complex V c) (i : ι) :
  C.boundaries i ≤ C.cycles i :=
image_le_kernel _ _ (C.d_to_comp_d_from i)

/--
The canonical map from `boundaries i` to `cycles i`.
-/
abbreviation boundaries_to_cycles (C : homological_complex V c) (i : ι) :
  (C.boundaries i : V) ⟶ (C.cycles i : V) :=
image_to_kernel _ _ (C.d_to_comp_d_from i)

/-- Prefer `boundaries_to_cycles`. -/
@[simp] lemma image_to_kernel_as_boundaries_to_cycles (C : homological_complex V c) (i : ι) (h) :
  (C.boundaries i).of_le (C.cycles i) h = C.boundaries_to_cycles i :=
rfl

variables [has_cokernels V]

/--
The homology of a complex at index `i`.
-/
abbreviation homology (C : homological_complex V c) (i : ι) : V :=
homology (C.d_to i) (C.d_from i) (C.d_to_comp_d_from i)

end

end homological_complex

open homological_complex

/-! Computing the cycles is functorial. -/
section
variables [has_zero_object V] [has_kernels V]
variables {C₁ C₂ C₃ : homological_complex V c} (f : C₁ ⟶ C₂)

/--
The morphism between cycles induced by a chain map.
-/
abbreviation cycles_map (f : C₁ ⟶ C₂) (i : ι) : (C₁.cycles i : V) ⟶ (C₂.cycles i : V) :=
subobject.factor_thru _ ((C₁.cycles i).arrow ≫ f.f i) (kernel_subobject_factors _ _ (by simp))

@[simp, reassoc, elementwise]
lemma cycles_map_arrow (f : C₁ ⟶ C₂) (i : ι) :
  (cycles_map f i) ≫ (C₂.cycles i).arrow = (C₁.cycles i).arrow ≫ f.f i :=
by { simp, }

@[simp] lemma cycles_map_id (i : ι) : cycles_map (𝟙 C₁) i = 𝟙 _ :=
by { dunfold cycles_map, simp, }

@[simp] lemma cycles_map_comp (f : C₁ ⟶ C₂) (g : C₂ ⟶ C₃) (i : ι) :
  cycles_map (f ≫ g) i = cycles_map f i ≫ cycles_map g i :=
by { dunfold cycles_map, simp [subobject.factor_thru_right], }

variables (V c)

/-- Cycles as a functor. -/
@[simps]
def cycles_functor (i : ι) : homological_complex V c ⥤ V :=
{ obj := λ C, C.cycles i,
  map := λ C₁ C₂ f, cycles_map f i, }

end

/-! Computing the boundaries is functorial. -/
section
variables [has_zero_object V] [has_images V] [has_image_maps V]
variables {C₁ C₂ C₃ : homological_complex V c} (f : C₁ ⟶ C₂)

/--
The morphism between boundaries induced by a chain map.
-/
abbreviation boundaries_map (f : C₁ ⟶ C₂) (i : ι) : (C₁.boundaries i : V) ⟶ (C₂.boundaries i : V) :=
image_subobject_map (f.sq_to i)

variables (V c)

/-- Boundaries as a functor. -/
@[simps]
def boundaries_functor (i : ι) : homological_complex V c ⥤ V :=
{ obj := λ C, C.boundaries i,
  map := λ C₁ C₂ f, image_subobject_map (f.sq_to i), }

end

section

/-! The `boundaries_to_cycles` morphisms are natural. -/
variables [has_zero_object V] [has_equalizers V] [has_images V] [has_image_maps V]
variables {C₁ C₂ : homological_complex V c} (f : C₁ ⟶ C₂)

@[simp, reassoc]
lemma boundaries_to_cycles_naturality (i : ι) :
  boundaries_map f i ≫ C₂.boundaries_to_cycles i = C₁.boundaries_to_cycles i ≫ cycles_map f i :=
by { ext, simp, }

variables (V c)

/-- The natural transformation from the boundaries functor to the cycles functor. -/
@[simps] def boundaries_to_cycles_nat_trans (i : ι) :
  boundaries_functor V c i ⟶ cycles_functor V c i :=
{ app := λ C, C.boundaries_to_cycles i,
  naturality' := λ C₁ C₂ f, boundaries_to_cycles_naturality f i, }

/-- The `i`-th homology, as a functor to `V`. -/
@[simps]
def homology_functor [has_cokernels V] (i : ι) :
  homological_complex V c ⥤ V :=
-- It would be nice if we could just write
-- `cokernel (boundaries_to_cycles_nat_trans V c i)`
-- here, but universe implementation details get in the way...
{ obj := λ C, C.homology i,
  map := λ C₁ C₂ f, _root_.homology.map _ _ (f.sq_to i) (f.sq_from i) rfl,
  map_id' :=
  begin
    intros, ext1,
    simp only [homology.π_map, kernel_subobject_map_id, hom.sq_from_id,
      category.id_comp, category.comp_id]
  end,
  map_comp' :=
  begin
    intros, ext1,
    simp only [hom.sq_from_comp, kernel_subobject_map_comp, homology.π_map_assoc,
      homology.π_map, category.assoc]
  end }

/-- The homology functor from `ι`-indexed complexes to `ι`-graded objects in `V`. -/
@[simps] def graded_homology_functor [has_cokernels V] :
  homological_complex V c ⥤ graded_object ι V :=
{ obj := λ C i, C.homology i,
  map := λ C C' f i, (homology_functor V c i).map f,
  map_id' :=
  begin
    intros, ext,
    simp only [pi.id_apply, homology.π_map, homology_functor_map, kernel_subobject_map_id,
      hom.sq_from_id, category.id_comp, category.comp_id]
  end,
  map_comp' :=
  begin
    intros, ext,
    simp only [hom.sq_from_comp, kernel_subobject_map_comp, homology.π_map_assoc,
      pi.comp_apply, homology.π_map, homology_functor_map, category.assoc]
  end }

end

author: nick-kuhn

repo: leantools

save_path: github-repos/lean/nick-kuhn-leantools


text:
import MyNat.Definition
import MyNat.Addition -- add_zero
import AdvancedAdditionWorld.Level6 -- add_left_cancel
namespace MyNat
open MyNat

/-!

# Advanced Addition World

## Level 8: `eq_zero_of_add_right_eq_self`

The lemma you're about to prove will be useful when we want to prove that `≤` is antisymmetric.
There are some wrong paths that you can take with this one.

## Lemma

If `a` and `b` are natural numbers such that
` a + b = a, ` then `b = 0`.
-/

lemma eq_zero_of_add_right_eq_self {a b : MyNat} : a + b = a → b = 0 := by
  intro h
  apply add_left_cancel a
  rw [h]
  rw [add_zero]

/-!
Remember from [FunctionWorld Level 4]()../FunctonWorld/Level4.lean.md) that the
`apply` tactic is can construct the path backwards?  Well when we use it with
`add_left_cancel a` it results in the opposite of cancellation, it
results in _adding a to both sides_ changing the goal from `⊢ b = 0`
to `⊢ a + b = a + 0`.  This then allows us to use our hypothesis `h : a + b = a`
in `rw` to complete the proof.

Next up [Level 9](./Level9.lean.md)
-/

author: leanprover