noncomputable def Set.IsCovering.glue_rel {α : Type u_1} {ι : Type u_3} {x : ι → Set α} (_h : Set.IsCovering x) (f : (i : ι) → Relation ↥(x i) ↥(x i)) : Relation α α

Equations

• _h.glue_rel f = {pair : α × α | ∃ (i : ι), ∃ (a : ↥(x i)), ∃ (b : ↥(x i)), (a, b) ∈ f i ∧ pair.fst = a.val ∧ pair.snd = b.val}

@[simp]

theorem Set.IsCovering.glue_rel_agrees {α : Type u_1} {ι : Type u_3} {i : ι} {x : ι → Set α} [RightDirected ↥(x '' Set.univ)] (h : Set.IsCovering x) {f : (i : ι) → Relation ↥(x i) ↥(x i)} (h' : ∀ (i j : ι) (sub : x i ⊆ x j) (a b : α) (ha : a ∈ x i) (hb : b ∈ x i), (⟨a, ha⟩, ⟨b, hb⟩) ∈ f i ↔ (⟨a, ⋯⟩, ⟨b, ⋯⟩) ∈ f j) (a b : α) (ha : a ∈ x i) (hb : b ∈ x i) : (a, b) ∈ h.glue_rel f ↔ (⟨a, ha⟩, ⟨b, hb⟩) ∈ f i

instance Set.isPreorderColimit {α : Type u_1} {ι : Type u_3} {x : ι → Set α} [RightDirected ↥(x '' Set.univ)] (h : Set.IsCovering x) {f : (i : ι) → Relation ↥(x i) ↥(x i)} [∀ (i : ι), IsPreorder (f i)] (h' : ∀ (i j : ι) (sub : x i ⊆ x j) (a b : α) (ha : a ∈ x i) (hb : b ∈ x i), (⟨a, ha⟩, ⟨b, hb⟩) ∈ f i ↔ (⟨a, ⋯⟩, ⟨b, ⋯⟩) ∈ f j) : IsPreorder (h.glue_rel f)

Equations

• ⋯ = ⋯

instance Set.isPartialOrderColimit {α : Type u_1} {ι : Type u_3} {x : ι → Set α} [RightDirected ↥(x '' Set.univ)] (h : Set.IsCovering x) {f : (i : ι) → Relation ↥(x i) ↥(x i)} [∀ (i : ι), IsPartialOrder (f i)] (h' : ∀ (i j : ι) (sub : x i ⊆ x j) (a b : α) (ha : a ∈ x i) (hb : b ∈ x i), (⟨a, ha⟩, ⟨b, hb⟩) ∈ f i ↔ (⟨a, ⋯⟩, ⟨b, ⋯⟩) ∈ f j) : IsPartialOrder (h.glue_rel f)

Equations

• ⋯ = ⋯

instance Set.isTotalOrderColimit {α : Type u_1} {ι : Type u_3} {x : ι → Set α} [RightDirected ↥(x '' Set.univ)] (h : Set.IsCovering x) {f : (i : ι) → Relation ↥(x i) ↥(x i)} [inst : ∀ (i : ι), IsTotalOrder (f i)] (h' : ∀ (i j : ι) (sub : x i ⊆ x j) (a b : α) (ha : a ∈ x i) (hb : b ∈ x i), (⟨a, ha⟩, ⟨b, hb⟩) ∈ f i ↔ (⟨a, ⋯⟩, ⟨b, ⋯⟩) ∈ f j) : IsTotalOrder (h.glue_rel f)

Equations

• ⋯ = ⋯