BooleanGap.lean

1import BFPP.ChainCompleteness2import Mathlib.Order.BooleanAlgebra.Basic34/-! # A gap in a maximal chain -/56namespace BFPP78set_option autoImplicit false9open Set1011variable (B : Type*) [Lattice B] [BoundedOrder B]1213/-- The order-theoretic gap before selecting cofinal ordinal sequences. -/14structure ChainGap where15  lower : Set B16  upper : Set B17  lower_chain : IsChain (· ≤ ·) lower18  upper_chain : IsChain (· ≤ ·) upper19  bot_mem : ⊥ ∈ lower20  top_mem : ⊤ ∈ upper21  cross : ∀ y ∈ lower, ∀ z ∈ upper, y ≤ z22  lower_no_max : ∀ y ∈ lower, ∃ y' ∈ lower, y < y'23  upper_no_min : ∀ z ∈ upper, ∃ z' ∈ upper, z' < z24  no_interpolant : ¬ ∃ b, (∀ y ∈ lower, y ≤ b) ∧ ∀ z ∈ upper, b ≤ z2526variable {B}2728theorem exists_chainGap (h : ∃ s : Set B, ¬ ∃ b, IsLUB s b) : Nonempty (ChainGap B) := by29  classical30  obtain ⟨c, hc, hn⟩ := exists_chain_without_isLUB h31  obtain ⟨M', hM', hcM⟩ := hc.exists_maxChain32  let M : Flag B := Flag.ofIsMaxChain M' hM'33  let Y : Set B := {y | y ∈ M ∧ ∃ a ∈ c, y ≤ a}34  let Z : Set B := {z | z ∈ M ∧ z ∉ Y}35  have hcY : c ⊆ Y := fun a ha => ⟨hcM ha, a, ha, le_rfl⟩36  have hnotub : ∀ y ∈ Y, y ∉ upperBounds c := by37    rintro y ⟨hyM, a, ha, hya⟩ hy38    apply hn39    exact ⟨y, hy, fun b hb => hya.trans (hb ha)⟩40  have hcross : ∀ y ∈ Y, ∀ z ∈ Z, y ≤ z := by41    rintro y ⟨hyM, a, ha, hya⟩ z ⟨hzM, hzY⟩42    rcases M.le_or_le hyM hzM with hyz | hzy43    · exact hyz44    · exact (hzY ⟨hzM, a, ha, hzy.trans hya⟩).elim45  have hYmax : ∀ y ∈ Y, ∃ y' ∈ Y, y < y' := by46    intro y hy47    have hbad := hnotub y hy48    change ¬ (∀ ⦃a⦄, a ∈ c → a ≤ y) at hbad49    push Not at hbad50    obtain ⟨a, ha, hay⟩ := hbad51    refine ⟨a, hcY ha, ?_⟩52    exact lt_of_le_not_ge ((M.le_or_le hy.1 (hcM ha)).resolve_right hay) hay53  have hZmin : ∀ z ∈ Z, ∃ z' ∈ Z, z' < z := by54    intro z hz55    by_contra hnone56    have hleast : ∀ z' ∈ Z, z ≤ z' := by57      intro z' hz'58      rcases M.le_or_le hz.1 hz'.1 with hzz | hzz59      · exact hzz60      · by_contra h61        exact hnone ⟨z', hz', lt_of_le_not_ge hzz h⟩62    have hzupper : z ∈ upperBounds c := fun a ha => hcross a (hcY ha) z hz63    apply hn64    refine ⟨z, hzupper, ?_⟩65    intro b hb66    have hmeetM : z ⊓ b ∈ M := by67      apply Flag.mem_iff_forall_le_or_ge.mpr68      intro m hm69      by_cases hmY : m ∈ Y70      · right71        obtain ⟨a, ha, hma⟩ := hmY.272        exact le_inf (hcross m hmY z hz) (hma.trans (hb ha))73      · exact Or.inl (inf_le_left.trans (hleast m ⟨hm, hmY⟩))74    have hmeetub : z ⊓ b ∈ upperBounds c := fun a ha => le_inf (hzupper ha) (hb ha)75    have hmeetZ : z ⊓ b ∈ Z := ⟨hmeetM, fun hY => hnotub _ hY hmeetub⟩76    exact (hleast _ hmeetZ).trans inf_le_right77  have hcne : c.Nonempty := by78    by_contra he79    rw [Set.not_nonempty_iff_eq_empty.mp he] at hn80    exact hn ⟨⊥, isLUB_empty⟩81  refine ⟨{82    lower := Y83    upper := Z84    lower_chain := M.chain_le.mono (fun _ h => h.1)85    upper_chain := M.chain_le.mono (fun _ h => h.1)86    bot_mem := ?_87    top_mem := ?_88    cross := hcross89    lower_no_max := hYmax90    upper_no_min := hZmin91    no_interpolant := ?_ }⟩92  · obtain ⟨a, ha⟩ := hcne93    exact ⟨M.bot_mem, a, ha, bot_le⟩94  · exact ⟨M.top_mem, fun ht => hnotub ⊤ ht (fun _ _ => le_top)⟩95  · rintro ⟨b, hYb, hbZ⟩96    have hbM : b ∈ M := by97      apply Flag.mem_iff_forall_le_or_ge.mpr98      intro m hm99      by_cases hmY : m ∈ Y100      · exact Or.inr (hYb m hmY)101      · exact Or.inl (hbZ m ⟨hm, hmY⟩)102    by_cases hbY : b ∈ Y103    · obtain ⟨b', hb', hlt⟩ := hYmax b hbY104      exact (not_le_of_gt hlt) (hYb b' hb')105    · obtain ⟨b', hb', hlt⟩ := hZmin b ⟨hbM, hbY⟩106      exact (not_le_of_gt hlt) (hbZ b' hb')107108end BFPP

SHA-256