Zulip Chat Archive

Stream: Is there code for X?

Topic: A bdd_above set of finsets is finite

Eric Wieser (Oct 25 2021 at 14:20):

Does this exist?

def bdd_below_aux {α} (f : finset α) (s : set α) [decidable_pred (∈ s)] : finset ↥s :=
(f.filter (∈ s)).attach.map $ (embedding.refl _).subtype_map $ λ x hx, (mem_filter.mp hx).2

lemma finite_of_mem_upper_bounds {f} {s : set (finset α)} (h : f ∈ upper_bounds s) : s.finite :=
begin
  rw mem_upper_bounds at h,
  refine ⟨_⟩,
  refine ⟨bdd_below_aux f.powerset s, _⟩,
  rintros ⟨x, hx⟩,
  simp [bdd_below_aux, embedding.subtype_map, embedding.refl, subtype.map],
  refine ⟨h _ hx, hx⟩,
end

lemma bdd_above.finite_of_finset {s : set (finset α)} (h : bdd_above s) : s.finite :=
let ⟨_, h⟩ := h in finite_of_mem_upper_bounds h

Yaël Dillies (Oct 25 2021 at 14:24):

Not quite! But you can get it by defining locally_finite_order (finset α)

Eric Wieser (Oct 25 2021 at 14:24):

docs#locally_finite_order?

Eric Wieser (Oct 25 2021 at 14:25):

Oh, interesting

Yaël Dillies (Oct 25 2021 at 14:25):

This is all new, so I haven't had time to define it.

Eric Wieser (Oct 25 2021 at 14:33):

For context, my goal was to try to define conditionally_complete_lattice (finset α) for non-finite α; but I suspect I can only populate Sup:

{ Sup := λ s, if h : s.finite then h.to_finset.sup id else ⊥,
  le_cSup := λ s fs sbdd hfs, begin
    have := sbdd.finite_of_finset,
    rw dif_pos this,
    convert finset.le_sup _,
    refl,
    simp [hfs],
  end,
  cSup_le := λ s fs sbdd hfs, begin
    have := finite_of_mem_upper_bounds hfs,
    rw dif_pos this,
    convert finset.sup_le _,
    intros b hb,
    apply hfs,
    rw set.finite.mem_to_finset at hb,
    exact hb,
  end,