From 6e9bc1c3e77ef62e656c98f20d3239116ea0cb8d Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 27 Mar 2023 00:51:35 +0000 Subject: [PATCH] feat: sync Data.Set.Intervals.OrdConnected (#3077) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Yaël Dillies --- Mathlib/Data/Set/Intervals/OrdConnected.lean | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/Mathlib/Data/Set/Intervals/OrdConnected.lean b/Mathlib/Data/Set/Intervals/OrdConnected.lean index 501b3c9021172..cb5c1004c2fb5 100644 --- a/Mathlib/Data/Set/Intervals/OrdConnected.lean +++ b/Mathlib/Data/Set/Intervals/OrdConnected.lean @@ -4,12 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Yury G. Kudryashov ! This file was ported from Lean 3 source module data.set.intervals.ord_connected -! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853 +! leanprover-community/mathlib commit b19481deb571022990f1baa9cbf9172e6757a479 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ import Mathlib.Data.Set.Intervals.UnorderedInterval import Mathlib.Data.Set.Lattice +import Mathlib.Order.Antichain /-! # Order-connected sets @@ -226,6 +227,19 @@ theorem dual_ordConnected {s : Set α} [OrdConnected s] : OrdConnected (ofDual end Preorder +section PartialOrder + +variable {α : Type _} [PartialOrder α] {s : Set α} + +protected theorem _root_.IsAntichain.ordConnected (hs : IsAntichain (· ≤ ·) s) : s.OrdConnected := + ⟨fun x hx y hy z hz => by + obtain rfl := hs.eq hx hy (hz.1.trans hz.2) + rw [Icc_self, mem_singleton_iff] at hz + rwa [hz]⟩ +#align is_antichain.ord_connected IsAntichain.ordConnected + +end PartialOrder + section LinearOrder variable {α : Type _} [LinearOrder α] {s : Set α} {x : α}