Having trouble with infi

Stream: new members

[Joe]

I was trying to prove the following:

[Joe]

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]

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]

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]

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]

Thanks!