Zulip Chat Archive

Stream: new members

Topic: Having trouble with infi


view this post on Zulip Joe (Jul 24 2019 at 07:10):

I was trying to prove the following:

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Joe (Jul 24 2019 at 07:55):

Thanks!


Last updated: May 13 2021 at 22:15 UTC