order_iso.map_cInf

Stream: Is there code for X?

[Yaël Dillies]

Do we have this or the subgoal anywhere?

import order.conditionally_complete_lattice

variables {α β γ : Type*} [conditionally_complete_lattice α] [conditionally_complete_lattice β]

lemma order_iso.map_cInf' (e : α ≃o β) {s : set α} (hne : s.nonempty) (hbdd : bdd_below s) :
  e (Inf s) = Inf (e '' s) :=
begin
  rw e.map_cInf hne hbdd,
  -- `⊢ (⨅ (x : ↥s), ⇑e ↑x) = Inf (⇑e '' s)`
end

[Yaël Dillies]

I did this in the end:

lemma cinfi_subtype {s : set β} {f : β → α} : (⨅ x : s, f x) = Inf (f '' s) :=
begin
  rw infi,
  congr,
  ext,
  rw [mem_image, mem_range, set_coe.exists],
  simp_rw [subtype.coe_mk, exists_prop],
end

lemma order_iso.map_cInf' (e : α ≃o β) {s : set α} (hne : s.nonempty) (hbdd : bdd_below s) :
  e (Inf s) = Inf (e '' s) :=
by rw [e.map_cInf hne hbdd, cinfi_subtype]

[Eric Wieser]

IMO docs#order_iso.map_cInf should have been written as the statement you're asking for.