Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(data/set/intervals): define set.ord_connected #3647

Closed
wants to merge 6 commits into from
Closed
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions src/data/set/intervals/ord_connected.lean
Original file line number Diff line number Diff line change
Expand Up @@ -10,9 +10,9 @@ import data.set.lattice
# Order-connected sets

We say that a set `s : set α` is `ord_connected` if for all `x y ∈ s` it includes the
interval `[x, y]`. If `α` is a `conditionally_complete_linear_order` with the `order_topology`,
then this condition is equivalent to `is_preconnected s`. If `α = ℝ`, then this condition is also
equivalent to `convex s`.
interval `[x, y]`. If `α` is a `denesly_ordered` `conditionally_complete_linear_order` with
sgouezel marked this conversation as resolved.
Show resolved Hide resolved
the `order_topology`, then this condition is equivalent to `is_preconnected s`. If `α = ℝ`, then
this condition is also equivalent to `convex s`.

In this file we prove that intersection of a family of `ord_connected` sets is `ord_connected` and
that all standard intervals are `ord_connected`.
Expand All @@ -24,9 +24,9 @@ variables {α : Type*} [preorder α] {s t : set α}

/--
We say that a set `s : set α` is `ord_connected` if for all `x y ∈ s` it includes the
interval `[x, y]`. If `α` is a `conditionally_complete_linear_order` with the `order_topology`,
then this condition is equivalent to `is_preconnected s`. If `α = ℝ`, then this condition is also
equivalent to `convex s`.
interval `[x, y]`. If `α` is a `denesly_ordered` `conditionally_complete_linear_order` with
sgouezel marked this conversation as resolved.
Show resolved Hide resolved
the `order_topology`, then this condition is equivalent to `is_preconnected s`. If `α = ℝ`, then
this condition is also equivalent to `convex s`.
-/
def ord_connected (s : set α) : Prop := ∀ ⦃x⦄ (hx : x ∈ s) ⦃y⦄ (hy : y ∈ s), Icc x y ⊆ s

Expand Down