## Stream: new members

### Topic: Having trouble with infi

#### Joe (Jul 24 2019 at 07:10):

I was trying to prove the following:

#### Joe (Jul 24 2019 at 07:10):

import order.conditionally_complete_lattice
import data.real.basic

open classical set lattice

variables {α : Type*} {β : Type*}
variables [conditionally_complete_linear_order α] {s t : set α} {a b : α}

lemma bar {K : set β} (ne : ∃ w, w ∈ K) {f : β → α} (h : (⨅ w ∈ K, f w) < a) : (∃w ∈ K, f w < a) :=
begin
sorry
end


Should be obvious, but I can't prove it.

#### Joe (Jul 24 2019 at 07:11):

I think there are some unintended behaviors of infi and supr on conditionally_complete_linear_order.
For example, when K is a nonempty set, (⨅ w ∈ K, (1:ℝ)) should be 1, but I can prove that it equals 0

#### Joe (Jul 24 2019 at 07:11):

open real

variables (Inf_one : real.Inf {(1:ℝ)} = 1)
(Inf_zero_one : real.Inf {(0:ℝ), (1:ℝ)} = 0)
include Inf_one Inf_zero_one

lemma foo {K : set ℕ} (h : K = {0}) : (⨅ w ∈ K, (1:ℝ)) = 0 :=
show real.Inf (range (λ w, real.Inf (range (λ (H : w ∈ K), (1:ℝ))))) = (0:ℝ), from
have h_range : range (λ w, real.Inf (range (λ (H : w ∈ K), (1:ℝ)))) = {(0:ℝ), (1:ℝ)},
begin
ext, rw mem_range, split,
rintros ⟨n, rfl⟩,
by_cases h₂ : n = (0:ℕ),
have : n ∈ K, finish,
have : range (λ (H : n ∈ K), (1:ℝ)) = {(1:ℝ)}, ext, finish,
rw [this, Inf_one], finish,

have : n ∉ K, finish,
have : range (λ (H : n ∈ K), (1:ℝ)) = (∅:set ℝ), ext, finish,
rw this, show lattice.Inf ∅ ∈ {(0:ℝ), (1:ℝ)}, rw real.Inf_empty, finish,

simp only [mem_singleton_iff, mem_insert_iff, set.insert_of_has_insert],
intro h, cases h with h h,
use 0,
have : range (λ (H : 0 ∈ K), (1:ℝ)) = {1}, ext, finish,
rw [this, Inf_one], finish,

use 1,
have : range (λ (H : 1 ∈ K), (1:ℝ)) = ∅, ext, finish,
rw this, show lattice.Inf ∅ = x, rw real.Inf_empty, finish
end,
begin
rw h_range, exact Inf_zero_one
end


#### Chris Hughes (Jul 24 2019 at 07:29):

The notation(⨅ w ∈ K, (1:ℝ)) doesn't mean what it looks like it means. It means this (⨅ w : ℕ, (⨅ H : w ∈ K, (1:ℝ))). Since the infinum of the empty set is zero (when it should really be the biggest real), this ends up being zero. You're obvious lemma isn't actually true I don't think. You could write (⨅ w : K, (1:ℝ)), and then it would be true.

#### Joe (Jul 24 2019 at 07:55):

Thanks!

Last updated: May 13 2021 at 22:15 UTC