## Stream: new members

### Topic: Add hypothesis to an instance

#### Christopher Hoskin (Jan 27 2021 at 19:10):

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 (Jan 27 2021 at 19:16):

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 (Jan 27 2021 at 19:19):

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 (Jan 27 2021 at 19:28):

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 (Jan 27 2021 at 19:29):

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 (Jan 27 2021 at 19:30):

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 (Jan 27 2021 at 21:51):

@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 (Jan 27 2021 at 22:17):

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 (Jan 27 2021 at 22:41):

@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 (Jan 27 2021 at 22:42):

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

#### Yakov Pechersky (Jan 27 2021 at 22:44):

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.

Last updated: May 09 2021 at 18:17 UTC