Add hypothesis to an instance

Stream: new members

[Christopher Hoskin]

Hello,

Given a topological space α, it's not too hard to show, using the results from topology.bounded_continuous_function that α →ᵇ ℝ, the space of bounded continuous real-valued functions on α, is a lattice in a natural way. I'm interested in the situation where the lattice structure on α →ᵇ ℝ is conditionally complete, which does not hold in general. I'm having difficulty seeing how to add this as a hypothesis. Naively I've tried:

import order.conditionally_complete_lattice
import topology.bounded_continuous_function

local infixr ` →ᵇ `:25 := bounded_continuous_function

universes u v

variables {α : Type u}

variables [topological_space α]

instance : lattice (α →ᵇ ℝ) := sorry

variables  (M : Type v) [nonempty M]

variables [conditionally_complete_lattice (α →ᵇ ℝ)]

lemma test1 (T:M→(α →ᵇ ℝ)) (l:(α →ᵇ ℝ)) (h: ∀ (x:M), (T x) ≤ l) : (⨆ (x:M), T x) ≤ l :=
begin
  apply csupr_le h,
end

But I get the error:

type mismatch at application
  csupr_le h
term
  h
has type
  ∀ (x : M), T x ≤ l
but is expected to have type
  ∀ (x : ?m_1), ?m_4 x ≤ ?m_5
state:
α : Type u,
_inst_1 : topological_space α,
M : Type v,
_inst_2 : nonempty M,
_inst_3 : conditionally_complete_lattice (α →ᵇ ℝ),
T : M → α →ᵇ ℝ,
l : α →ᵇ ℝ,
h : ∀ (x : M), T x ≤ l
⊢ (⨆ (x : M), T x) ≤ l

(I've replaced the proof that α →ᵇ ℝ is a lattice with sorry in the above for brevity.)

If I comment out the line instance : lattice (α →ᵇ ℝ) := sorry then there are no errors.

How do I say "given this structure which we've proved to be a lattice, add the hypothesis that the lattice is conditionally complete"?

Thanks,

Christopher

[Bryan Gin-ge Chen]

The conditionally_complete_lattice instance already contains the data of a lattice structure (see the fields available in docs#conditionally_complete_lattice), so having a separate lattice instance on the same type confuses Lean.

[Christopher Hoskin]

Yes, something like this works in Lean (but is mathematically incorrect):

instance : conditionally_complete_lattice (α →ᵇ ℝ) := {
  Sup := sorry,
  Inf := sorry,
  le_cSup := sorry,
  cSup_le := sorry,
  cInf_le := sorry,
  le_cInf := sorry,
  ..bounded_continuous_function.lattice,
}

I think I'm looking for something which replaces these sorrys with "take this as an hypothesis".

[Christopher Hoskin]

Perhaps it would be clearer if I gave an example? Given a compact Hausdorff space α, if the lattice (α →ᵇ ℝ) is conditionally complete, then α is Stonean.

[Alex J. Best]

Maybe this does what you want:

import order.conditionally_complete_lattice
import topology.bounded_continuous_function

local infixr ` →ᵇ `:25 := bounded_continuous_function

universes u v
noncomputable theory
variables {α : Type u}

variables [topological_space α]

instance : lattice (α →ᵇ ℝ) := sorry

variables  (M : Type v) [nonempty M]
variable (α)
class my_mixin [lattice α] :=
(Sup : set α → α)
(Inf : set α → α)
(le_cSup : ∀ (s : set α) (a : α), bdd_above s → a ∈ s → a ≤ Sup s)
(cSup_le : ∀ (s : set α) (a : α), s.nonempty → a ∈ upper_bounds s → Sup s ≤ a)
(cInf_le : ∀ (s : set α) (a : α), bdd_below s → a ∈ s → Inf s ≤ a)
(le_cInf : ∀ (s : set α) (a : α), s.nonempty → a ∈ lower_bounds s → a ≤ Inf s)
#check my_mixin
variable {α}
instance [h : my_mixin (α →ᵇ ℝ)] : conditionally_complete_lattice (α →ᵇ ℝ) :=
{ .. h,
.. (by apply_instance : lattice (α →ᵇ ℝ)) }
variable [my_mixin (α →ᵇ ℝ)]
lemma test1 (T:M→(α →ᵇ ℝ)) (l:(α →ᵇ ℝ)) (h: ∀ (x:M), (T x) ≤ l) : (⨆ (x:M), T x) ≤ l :=
begin
  apply csupr_le h,
end

[Alex J. Best]

You make a new class with the missing fields, parameterised by lattice structures, then assume one of those and make an instance from the new class to the thing you actually want to assume.

[Christopher Hoskin]

@Alex J. Best Thank you. A bit clunky perhaps, but this seems to work:

import order.conditionally_complete_lattice
import topology.bounded_continuous_function

local infixr ` →ᵇ `:25 := bounded_continuous_function

universes u v
variables {α : Type u}

variables [topological_space α]

instance : lattice (α →ᵇ ℝ) := sorry

variables  (M : Type v) [nonempty M]

variable (L : Type*)

class conditionally_complete [lattice L] :=
(Sup : set L → L)
(Inf : set L → L)
(le_cSup : ∀ (s : set L) (a : L), bdd_above s → a ∈ s → a ≤ Sup s)
(cSup_le : ∀ (s : set L) (a : L), s.nonempty → a ∈ upper_bounds s → Sup s ≤ a)
(cInf_le : ∀ (s : set L) (a : L), bdd_below s → a ∈ s → Inf s ≤ a)
(le_cInf : ∀ (s : set L) (a : L), s.nonempty → a ∈ lower_bounds s → a ≤ Inf s)

variable [lattice L]

instance conditionally_complete_lattice2 [h: conditionally_complete L]  : conditionally_complete_lattice L :=
{ .. h,
.. (by apply_instance : lattice L) }

lemma test1 [h: conditionally_complete (α →ᵇ ℝ) ] (T:M→(α →ᵇ ℝ)) (l:(α →ᵇ ℝ))
(h: ∀ (x:M), (T x) ≤ l) : (⨆ (x:M), T x) ≤ l :=
begin
  apply csupr_le h,
end

[Yakov Pechersky]

The proof at the end is just the term proof csupr_le h. There is already a docs#conditionally_complete_lattice_of_complete_lattice.

[Christopher Hoskin]

@Yakov Pechersky conditionally_complete_lattice_of_complete_lattice shows that a complete lattice is always conditionally complete. I'm looking to impose the conditionally complete hypothesis on a (not necessarily complete) lattice.

[Christopher Hoskin]

(The result at the end is just a trivial example.)

[Yakov Pechersky]

Ah I see -- makes sense! I'm surprised there isn't a clean way of using some sort of def to get this instance. But I see that's exactly the subtype of bdd_cont_functions you're working with.