IndexedGaps.lean

1import BFPP.BooleanGap2import BFPP.CofinalSequences34/-! # Cofinal ordinal coordinates for a lattice gap -/56namespace BFPP78set_option autoImplicit false9open Set Order1011universe u v w12variable (B : Type u) (ι : Type v) (κ : Type w)13  [Lattice B] [BoundedOrder B] [LinearOrder ι] [OrderBot ι] [LinearOrder κ] [OrderBot κ]1415structure IndexedGap where16  lower : ι → B17  upper : κ → B18  lower_mono : Monotone lower19  upper_anti : Antitone upper20  lower_bot : lower ⊥ = ⊥21  upper_bot : upper ⊥ = ⊤22  cross : ∀ i j, lower i ≤ upper j23  no_interpolant : ¬ ∃ b, (∀ i, lower i ≤ b) ∧ ∀ j, b ≤ upper j2425namespace ChainGap2627variable {B ι κ}2829noncomputable instance lowerLinearOrder (g : ChainGap B) : LinearOrder g.lower := by30  classical31  exact { Subtype.partialOrder _ with32    le_total := fun a b => g.lower_chain.total a.property b.property33    toDecidableLE := Classical.decRel _ }3435noncomputable instance upperLinearOrder (g : ChainGap B) : LinearOrder g.upper := by36  classical37  exact { Subtype.partialOrder _ with38    le_total := fun a b => g.upper_chain.total a.property b.property39    toDecidableLE := Classical.decRel _ }4041instance lowerOrderBot (g : ChainGap B) : OrderBot g.lower := Subtype.orderBot g.bot_mem42instance upperOrderTop (g : ChainGap B) : OrderTop g.upper := Subtype.orderTop g.top_mem4344instance lowerNoMaxOrder (g : ChainGap B) : NoMaxOrder g.lower := ⟨by45  intro a46  obtain ⟨b, hb, hab⟩ := g.lower_no_max a.val a.property47  exact ⟨⟨b, hb⟩, hab⟩⟩4849instance upperNoMinOrder (g : ChainGap B) : NoMinOrder g.upper := ⟨by50  intro a51  obtain ⟨b, hb, hab⟩ := g.upper_no_min a.val a.property52  exact ⟨⟨b, hb⟩, hab⟩⟩5354theorem exists_indexedGap (g : ChainGap B) :55    ∃ ρ σ : Ordinal.{u}, ∃ hρ : IsSuccLimit ρ, ∃ hσ : IsSuccLimit σ,56      ρ.cof.ord = ρ ∧ σ.cof.ord = σ ∧57      @Nonempty (@IndexedGap B (OrdinalIndex ρ) (OrdinalIndex σ) _ _ _58        (@ordinalIndexOrderBot ρ ⟨hρ⟩) _ (@ordinalIndexOrderBot σ ⟨hσ⟩)) := by59  obtain ⟨ρ, hρ, hregρ, f, hf, hf₀, hfcof⟩ := exists_regular_cofinal_sequence_from_bot g.lower60  obtain ⟨σ, hσ, hregσ, h, hh, hh₀, hhcof⟩ :=61    exists_regular_cofinal_sequence_from_bot (OrderDual g.upper)62  letI : Fact (IsSuccLimit ρ) := ⟨hρ⟩63  letI : Fact (IsSuccLimit σ) := ⟨hσ⟩64  refine ⟨ρ, σ, hρ, hσ, hregρ, hregσ, ⟨{65    lower := fun i => (f i).val66    upper := fun j => (h j).val67    lower_mono := fun _ _ hij => hf hij68    upper_anti := fun _ _ hij => hh hij69    lower_bot := ?_70    upper_bot := ?_71    cross := fun i j => g.cross _ (f i).property _ (h j).property72    no_interpolant := ?_ }⟩⟩73  · exact congrArg Subtype.val hf₀74  · exact congrArg Subtype.val hh₀75  · rintro ⟨b, hfb, hbh⟩76    apply g.no_interpolant77    refine ⟨b, ?_, ?_⟩78    · intro y hy79      obtain ⟨_, ⟨i, rfl⟩, hyi⟩ := hfcof ⟨y, hy⟩80      change y ≤ (f i).val at hyi81      exact hyi.trans (hfb i)82    · intro z hz83      obtain ⟨_, ⟨j, rfl⟩, hjz⟩ := hhcof ⟨z, hz⟩84      change (h j).val ≤ z at hjz85      exact (hbh j).trans hjz8687end ChainGap88end BFPP

SHA-256