infimum of bdd_below int set

Stream: new members

[Yakov Pechersky]

What's the right way to invoke Inf on a set int when I know it is nonempty and bdd_below?

import group_theory.subgroup

example (H : add_subgroup ℤ) (x : ℤ) (hx : x ∈ H) (xpos : 0 < x) :
  ∃! (b : ℤ), 0 < b ∧ b ∈ H ∧ (∀ (c ∈ H), 0 < c → b ≤ c) :=
begin
  set bs : set ℤ := {b : ℤ | b ∈ H ∧ 0 < b} with hbs,
  have bsbdd : bdd_below bs,
  { use 0,
    simp_rw [mem_lower_bounds, hbs, set.mem_set_of_eq, and_imp],
    intros x hx xpos,
    exact xpos.le },
  have bsnonempty : bs.nonempty := ⟨x, hx, xpos⟩,
  use (Inf bs), -- fails here
  sorry
end

[Eric Wieser]

Wait for Floris' PR?

[Yakov Pechersky]

Which one is that?

[Eric Wieser]

#8149

[Eric Wieser]

I fixed some whitespace and was rewarded with a deterministic timeout

[Yakov Pechersky]

OK, at least that PR taught me something new, which I can use in the meantime:

import group_theory.subgroup

example (H : add_subgroup ℤ) (x : ℤ) (hx : x ∈ H) (xpos : 0 < x) :
  ∃! (b : ℤ), 0 < b ∧ b ∈ H ∧ (∀ (c ∈ H), 0 < c → b ≤ c) :=
begin
  set bs : set ℤ := {b : ℤ | b ∈ H ∧ 0 < b} with hbs,
  classical,
  obtain ⟨lb, hlb, hlb'⟩ := @int.exists_least_of_bdd (∈ bs) ⟨0, λ z hz, hz.right.le⟩ ⟨x, hx, xpos⟩,
  simp only [and_imp, set.mem_set_of_eq] at hlb hlb',
  refine ⟨lb, ⟨hlb.right, hlb.left, hlb'⟩, _⟩,
  simp only [and_imp],
  intros c cpos hc IH,
  exact le_antisymm (IH _ hlb.left hlb.right) (hlb' _ hc cpos)
end

[Yakov Pechersky]

@Eric Wieser I've hit that timeout before, in that exact lemma. I've tried to break it up into pieces, but have failed. It really abuses defeq across quotients.