# Zulip Chat Archive

## 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