Chains and flags #

theorem is_chain.mono_rel {α : Type u_1} {r : α → α → Prop} {s : set α} {r' : α → α → Prop} (h : is_chain r s) (h_imp : ∀ (x y : α), r x y → r' x y) :

is_chain r' s

source

theorem is_chain.symm {α : Type u_1} {r : α → α → Prop} {s : set α} (h : is_chain r s) :

is_chain (flip r) s

This can be used to turn is_chain (≥) into is_chain (≤) and vice-versa.

source

theorem is_chain_of_trichotomous {α : Type u_1} {r : α → α → Prop} [is_trichotomous α r] (s : set α) :

is_chain r s

source

theorem is_chain.insert {α : Type u_1} {r : α → α → Prop} {s : set α} {a : α} (hs : is_chain r s) (ha : ∀ (b : α), b ∈ s → a ≠ b → r a b ∨ r b a) :

is_chain r (has_insert.insert a s)

source

theorem is_chain_univ_iff {α : Type u_1} {r : α → α → Prop} :

is_chain r set.univ ↔ is_trichotomous α r

source

theorem is_chain.image {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) (f : α → β) (h : ∀ (x y : α), r x y → s (f x) (f y)) {c : set α} (hrc : is_chain r c) :

is_chain s (f '' c)

source

theorem is_chain.total {α : Type u_1} {r : α → α → Prop} {s : set α} {x y : α} [is_refl α r] (h : is_chain r s) (hx : x ∈ s) (hy : y ∈ s) :

r x y ∨ r y x

source

theorem is_chain.directed_on {α : Type u_1} {r : α → α → Prop} {s : set α} [is_refl α r] (H : is_chain r s) :

directed_on r s

source

@[protected]

theorem is_chain.directed {α : Type u_1} {β : Type u_2} {r : α → α → Prop} [is_refl α r] {f : β → α} {c : set β} (h : is_chain (f ⁻¹'o r) c) :

directed r (λ (x : {a // a ∈ c}), f ↑x)

source

theorem is_chain.exists3 {α : Type u_1} {r : α → α → Prop} {s : set α} [is_refl α r] (hchain : is_chain r s) [is_trans α r] {a b c : α} (mem1 : a ∈ s) (mem2 : b ∈ s) (mem3 : c ∈ s) :

∃ (z : α) (mem4 : z ∈ s), r a z ∧ r b z ∧ r c z

source

theorem is_max_chain.is_chain {α : Type u_1} {r : α → α → Prop} {s : set α} (h : is_max_chain r s) :

is_chain r s

source

theorem is_max_chain.not_super_chain {α : Type u_1} {r : α → α → Prop} {s t : set α} (h : is_max_chain r s) :

¬super_chain r s t

source

theorem is_max_chain.bot_mem {α : Type u_1} {s : set α} [has_le α] [order_bot α] (h : is_max_chain has_le.le s) :

⊥ ∈ s

source

theorem is_max_chain.top_mem {α : Type u_1} {s : set α} [has_le α] [order_top α] (h : is_max_chain has_le.le s) :

⊤ ∈ s

source

def succ_chain {α : Type u_1} (r : α → α → Prop) (s : set α) :

set α

Given a set s, if there exists a chain t strictly including s, then succ_chain s is one of these chains. Otherwise it is s.

Equations

succ_chain r s = dite (∃ (t : set α), is_chain r s ∧ super_chain r s t) (λ (h : ∃ (t : set α), is_chain r s ∧ super_chain r s t), classical.some h) (λ (h : ¬∃ (t : set α), is_chain r s ∧ super_chain r s t), s)

source

theorem succ_chain_spec {α : Type u_1} {r : α → α → Prop} {s : set α} (h : ∃ (t : set α), is_chain r s ∧ super_chain r s t) :

super_chain r s (succ_chain r s)

source

theorem is_chain.succ {α : Type u_1} {r : α → α → Prop} {s : set α} (hs : is_chain r s) :

is_chain r (succ_chain r s)

source

theorem is_chain.super_chain_succ_chain {α : Type u_1} {r : α → α → Prop} {s : set α} (hs₁ : is_chain r s) (hs₂ : ¬is_max_chain r s) :

super_chain r s (succ_chain r s)

source

theorem subset_succ_chain {α : Type u_1} {r : α → α → Prop} {s : set α} :

s ⊆ succ_chain r s

source

inductive chain_closure {α : Type u_1} (r : α → α → Prop) :

set α → Prop

succ : ∀ {α : Type u_1} {r : α → α → Prop} {s : set α}, chain_closure r s → chain_closure r (succ_chain r s)
union : ∀ {α : Type u_1} {r : α → α → Prop} {s : set (set α)}, (∀ (a : set α), a ∈ s → chain_closure r a) → chain_closure r (⋃₀ s)

Predicate for whether a set is reachable from ∅ using succ_chain and ⋃₀.

source

def max_chain {α : Type u_1} (r : α → α → Prop) :

set α

An explicit maximal chain. max_chain is taken to be the union of all sets in chain_closure.

Equations

max_chain r = ⋃₀ set_of (chain_closure r)

source

theorem chain_closure_empty {α : Type u_1} {r : α → α → Prop} :

chain_closure r ∅

source

theorem chain_closure_max_chain {α : Type u_1} {r : α → α → Prop} :

chain_closure r (max_chain r)

source

theorem chain_closure.total {α : Type u_1} {r : α → α → Prop} {c₁ c₂ : set α} (hc₁ : chain_closure r c₁) (hc₂ : chain_closure r c₂) :

c₁ ⊆ c₂ ∨ c₂ ⊆ c₁

source

theorem chain_closure.succ_fixpoint {α : Type u_1} {r : α → α → Prop} {c₁ c₂ : set α} (hc₁ : chain_closure r c₁) (hc₂ : chain_closure r c₂) (hc : succ_chain r c₂ = c₂) :

c₁ ⊆ c₂

source

theorem chain_closure.succ_fixpoint_iff {α : Type u_1} {r : α → α → Prop} {c : set α} (hc : chain_closure r c) :

succ_chain r c = c ↔ c = max_chain r

source

theorem chain_closure.is_chain {α : Type u_1} {r : α → α → Prop} {c : set α} (hc : chain_closure r c) :

is_chain r c

source

theorem max_chain_spec {α : Type u_1} {r : α → α → Prop} :

is_max_chain r (max_chain r)

Hausdorff's maximality principle

There exists a maximal totally ordered set of α. Note that we do not require α to be partially ordered by r.

Flags #

source

structure flag (α : Type u_3) [has_le α] :

Type u_3

carrier : set α
chain' : is_chain has_le.le self.carrier
max_chain' : ∀ ⦃s : set α⦄, is_chain has_le.le s → self.carrier ⊆ s → self.carrier = s

The type of flags, aka maximal chains, of an order.

Instances for flag

flag.has_sizeof_inst
flag.set_like
flag.unique

source

@[protected, instance]

def flag.set_like {α : Type u_1} [has_le α] :

set_like (flag α) α

Equations

flag.set_like = {coe := flag.carrier _inst_1, coe_injective' := _}

source

@[ext]

theorem flag.ext {α : Type u_1} [has_le α] {s t : flag α} :

↑s = ↑t → s = t

source

@[simp]

theorem flag.mem_coe_iff {α : Type u_1} [has_le α] {s : flag α} {a : α} :

a ∈ ↑s ↔ a ∈ s

source

@[simp]

theorem flag.coe_mk {α : Type u_1} [has_le α] (s : set α) (h₁ : is_chain has_le.le s) (h₂ : ∀ ⦃s_1 : set α⦄, is_chain has_le.le s_1 → s ⊆ s_1 → s = s_1) :

↑{carrier := s, chain' := h₁, max_chain' := h₂} = s

source

@[simp]