feat(order/cover): f a covers f b iff a covers b (#11392)

... for order isomorphisms, and also weaker statements.

Co-authored-by: Vladimir Ivanov <@astOwOlfo>

src/order/cover.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Violeta Hernández Palacios, Grayson Burton
 -/
-import data.set.intervals.basic
+import data.set.intervals.ord_connected
 
 /-!
 # The covering relation
@@ -18,7 +18,7 @@ is no element in between. ∃ b, a < b
 
 open set
 
-variables {α : Type*}
+variables {α β : Type*}
 
 section has_lt
 variables [has_lt α] {a b : α}
@@ -34,30 +34,69 @@ lemma covers.lt (h : a ⋖ b) : a < b := h.1
 lemma not_covers_iff (h : a < b) : ¬a ⋖ b ↔ ∃ c, a < c ∧ c < b :=
 by { simp_rw [covers, not_and, not_forall, exists_prop, not_not], exact imp_iff_right h }
 
+alias not_covers_iff ↔ exists_lt_lt_of_not_covers _
+alias exists_lt_lt_of_not_covers ← has_lt.lt.exists_lt_lt
+
+/-- In a dense order, nothing covers anything. -/
+lemma not_covers [densely_ordered α] : ¬ a ⋖ b :=
+λ h, let ⟨c, hc⟩ := exists_between h.1 in h.2 hc.1 hc.2
+
+lemma densely_ordered_iff_forall_not_covers : densely_ordered α ↔ ∀ a b : α, ¬ a ⋖ b :=
+⟨λ h a b, @not_covers _ _ _ _ h, λ h, ⟨λ a b hab, exists_lt_lt_of_not_covers hab $ h _ _⟩⟩
+
 open order_dual
 
 @[simp] lemma to_dual_covers_to_dual_iff : to_dual b ⋖ to_dual a ↔ a ⋖ b :=
 and_congr_right' $ forall_congr $ λ c, forall_swap
 
-alias to_dual_covers_to_dual_iff ↔ _ covers.to_dual
+@[simp] lemma of_dual_covers_of_dual_iff {a b : order_dual α} :
+  of_dual a ⋖ of_dual b ↔ b ⋖ a :=
+and_congr_right' $ forall_congr $ λ c, forall_swap
 
-/-- In a dense order, nothing covers anything. -/
-lemma not_covers [densely_ordered α] : ¬ a ⋖ b :=
-λ h, let ⟨c, hc⟩ := exists_between h.1 in h.2 hc.1 hc.2
+alias to_dual_covers_to_dual_iff ↔ _ covers.to_dual
+alias of_dual_covers_of_dual_iff ↔ _ covers.of_dual
 
 end has_lt
 
 section preorder
-variables [preorder α] {a b : α}
+variables [preorder α] [preorder β] {a b : α} {f : α ↪o β} {e : α ≃o β}
 
 lemma covers.le (h : a ⋖ b) : a ≤ b := h.1.le
 protected lemma covers.ne (h : a ⋖ b) : a ≠ b := h.lt.ne
 lemma covers.ne' (h : a ⋖ b) : b ≠ a := h.lt.ne'
 
+instance covers.is_irrefl : is_irrefl α (⋖) := ⟨λ a ha, ha.ne rfl⟩
+
 lemma covers.Ioo_eq (h : a ⋖ b) : Ioo a b = ∅ :=
 eq_empty_iff_forall_not_mem.2 $ λ x hx, h.2 hx.1 hx.2
 
-instance covers.is_irrefl : is_irrefl α (⋖) := ⟨λ a ha, ha.ne rfl⟩
+lemma covers.of_image (h : f a ⋖ f b) : a ⋖ b :=
+begin
+  refine ⟨_, λ c hac hcb, _⟩,
+  { rw ←order_embedding.lt_iff_lt f,
+    exact h.1 },
+  rw ←order_embedding.lt_iff_lt f at hac hcb,
+  exact h.2 hac hcb,
+end
+
+lemma covers.image (hab : a ⋖ b) (h : (set.range f).ord_connected) : f a ⋖ f b :=
+begin
+  refine ⟨f.strict_mono hab.1, λ c ha hb, _⟩,
+  obtain ⟨c, rfl⟩ := h.out (mem_range_self _) (mem_range_self _) ⟨ha.le, hb.le⟩,
+  rw f.lt_iff_lt at ha hb,
+  exact hab.2 ha hb,
+end
+
+protected lemma set.ord_connected.image_covers_image_iff (h : (set.range f).ord_connected) :
+  f a ⋖ f b ↔ a ⋖ b :=
+⟨covers.of_image, λ hab, hab.image h⟩
+
+@[simp] lemma apply_covers_apply_iff : e a ⋖ e b ↔ a ⋖ b :=
+⟨covers.of_image, λ hab, begin
+  refine ⟨e.strict_mono hab.1, λ c ha hb, _⟩,
+  rw [←e.symm.lt_iff_lt, order_iso.symm_apply_apply] at ha hb,
+  exact hab.2 ha hb,
+end⟩
 
 end preorder