feat : new properties of the CardinalInterFilter (#11758)

extend more of the API from CountableInterFilter
to CardinalInterFilter




Co-authored-by: Oliver Nash <github@olivernash.org>

Author: JADekker

Mathlib/Order/Filter/CardinalInter.lean

@@ -6,6 +6,7 @@ Authors: Josha Dekker
 import Mathlib.Order.Filter.Basic
 import Mathlib.Order.Filter.CountableInter
 import Mathlib.SetTheory.Cardinal.Ordinal
+import Mathlib.SetTheory.Cardinal.Cofinality
 
 /-!
 # Filters with a cardinal intersection property
@@ -73,12 +74,16 @@ theorem cardinalInterFilter_aleph_one_iff :
     CardinalInterFilter.cardinal_sInter_mem S ((countable_iff_lt_aleph_one S).1 h) a⟩,
    fun _ ↦ CountableInterFilter.toCardinalInterFilter l⟩
 
-/-- Every CardinalInterFilter for some c also is a CardinalInterFilter for some a < c -/
-theorem CardinalInterFilter.of_CardinalInterFilter_of_lt (l : Filter α) [CardinalInterFilter l c]
-    {a : Cardinal.{u}} (hac : a < c) :
+/-- Every CardinalInterFilter for some c also is a CardinalInterFilter for some a ≤ c -/
+theorem CardinalInterFilter.of_cardinalInterFilter_of_le (l : Filter α) [CardinalInterFilter l c]
+    {a : Cardinal.{u}} (hac : a ≤ c) :
   CardinalInterFilter l a where
     cardinal_sInter_mem :=
-      fun S hS a ↦ CardinalInterFilter.cardinal_sInter_mem S (lt_trans hS hac) a
+      fun S hS a ↦ CardinalInterFilter.cardinal_sInter_mem S (lt_of_lt_of_le hS hac) a
+
+theorem CardinalInterFilter.of_cardinalInterFilter_of_lt (l : Filter α) [CardinalInterFilter l c]
+    {a : Cardinal.{u}} (hac : a < c) : CardinalInterFilter l a :=
+  CardinalInterFilter.of_cardinalInterFilter_of_le l (hac.le)
 
 namespace Filter
 
@@ -87,8 +92,7 @@ variable [CardinalInterFilter l c]
 theorem cardinal_iInter_mem {s : ι → Set α} (hic : #ι < c) :
     (⋂ i, s i) ∈ l ↔ ∀ i, s i ∈ l := by
   rw [← sInter_range _]
-  apply Iff.trans
-  apply cardinal_sInter_mem (lt_of_le_of_lt Cardinal.mk_range_le hic)
+  apply (cardinal_sInter_mem (lt_of_le_of_lt Cardinal.mk_range_le hic)).trans
   exact forall_mem_range
 
 theorem cardinal_bInter_mem {S : Set ι} (hS : #S < c)
@@ -152,4 +156,184 @@ theorem EventuallyEq.cardinal_bInter {S : Set ι} (hS : #S < c)
   (EventuallyLE.cardinal_bInter hS fun i hi => (h i hi).le).antisymm
     (EventuallyLE.cardinal_bInter hS fun i hi => (h i hi).symm.le)
 
+/-- Construct a filter with cardinal `c` intersection property. This constructor deduces
+`Filter.univ_sets` and `Filter.inter_sets` from the cardinal `c` intersection property. -/
+def ofCardinalInter (l : Set (Set α)) (hc : 2 < c)
+    (hl : ∀ S : Set (Set α), (#S < c) → S ⊆ l → ⋂₀ S ∈ l)
+    (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) : Filter α where
+  sets := l
+  univ_sets :=
+    sInter_empty ▸ hl ∅ (mk_eq_zero (∅ : Set (Set α)) ▸ lt_trans zero_lt_two hc) (empty_subset _)
+  sets_of_superset := h_mono _ _
+  inter_sets {s t} hs ht := sInter_pair s t ▸ by
+    apply hl _ (?_) (insert_subset_iff.2 ⟨hs, singleton_subset_iff.2 ht⟩)
+    have : #({s, t} : Set (Set α)) ≤ 2 := by
+      calc
+      _ ≤ #({t} : Set (Set α)) + 1 := Cardinal.mk_insert_le
+      _ = 2 := by norm_num
+    exact lt_of_le_of_lt this hc
+
+instance cardinalInter_ofCardinalInter (l : Set (Set α)) (hc : 2 < c)
+    (hl : ∀ S : Set (Set α), (#S < c) → S ⊆ l → ⋂₀ S ∈ l)
+    (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) :
+    CardinalInterFilter (Filter.ofCardinalInter l hc hl h_mono) c :=
+  ⟨hl⟩
+
+@[simp]
+theorem mem_ofCardinalInter {l : Set (Set α)} (hc : 2 < c)
+    (hl : ∀ S : Set (Set α), (#S < c) → S ⊆ l → ⋂₀ S ∈ l) (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l)
+    {s : Set α} : s ∈ Filter.ofCardinalInter l hc hl h_mono ↔ s ∈ l :=
+  Iff.rfl
+
+/-- Construct a filter with cardinal `c` intersection property.
+Similarly to `Filter.comk`, a set belongs to this filter if its complement satisfies the property.
+Similarly to `Filter.ofCardinalInter`,
+this constructor deduces some properties from the cardinal `c` intersection property
+which becomes the cardinal `c` union property because we take complements of all sets. -/
+def ofCardinalUnion (l : Set (Set α)) (hc : 2 < c)
+    (hUnion : ∀ S : Set (Set α), (#S < c) → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l)
+    (hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l) : Filter α := by
+  refine .ofCardinalInter {s | sᶜ ∈ l} hc (fun S hSc hSp ↦ ?_) fun s t ht hsub ↦ ?_
+  · rw [mem_setOf_eq, compl_sInter]
+    apply hUnion (compl '' S) (lt_of_le_of_lt mk_image_le hSc)
+    intro s hs
+    rw [mem_image] at hs
+    rcases hs with ⟨t, ht, rfl⟩
+    apply hSp ht
+  · rw [mem_setOf_eq]
+    rw [← compl_subset_compl] at hsub
+    exact hmono sᶜ ht tᶜ hsub
+
+instance cardinalInter_ofCardinalUnion (l : Set (Set α)) (hc : 2 < c) (h₁ h₂) :
+    CardinalInterFilter (Filter.ofCardinalUnion l hc h₁ h₂) c :=
+  cardinalInter_ofCardinalInter ..
+
+@[simp]
+theorem mem_ofCardinalUnion {l : Set (Set α)} (hc : 2 < c) {hunion hmono s} :
+    s ∈ ofCardinalUnion l hc hunion hmono ↔ l sᶜ :=
+  Iff.rfl
+
+instance cardinalInterFilter_principal (s : Set α) : CardinalInterFilter (𝓟 s) c :=
+  ⟨fun _ _ hS => subset_sInter hS⟩
+
+instance cardinalInterFilter_bot : CardinalInterFilter (⊥ : Filter α) c := by
+  rw [← principal_empty]
+  apply cardinalInterFilter_principal
+
+instance cardinalInterFilter_top : CardinalInterFilter (⊤ : Filter α) c := by
+  rw [← principal_univ]
+  apply cardinalInterFilter_principal
+
+instance (l : Filter β) [CardinalInterFilter l c] (f : α → β) :
+    CardinalInterFilter (comap f l) c := by
+  refine ⟨fun S hSc hS => ?_⟩
+  choose! t htl ht using hS
+  refine ⟨_, (cardinal_bInter_mem hSc).2 htl, ?_⟩
+  simpa [preimage_iInter] using iInter₂_mono ht
+
+instance (l : Filter α) [CardinalInterFilter l c] (f : α → β) :
+    CardinalInterFilter (map f l) c := by
+  refine ⟨fun S hSc hS => ?_⟩
+  simp only [mem_map, sInter_eq_biInter, preimage_iInter₂] at hS ⊢
+  exact (cardinal_bInter_mem hSc).2 hS
+
+/-- Infimum of two `CardinalInterFilter`s is a `CardinalInterFilter`. This is useful, e.g.,
+to automatically get an instance for `residual α ⊓ 𝓟 s`. -/
+instance cardinalInterFilter_inf_eq (l₁ l₂ : Filter α) [CardinalInterFilter l₁ c]
+    [CardinalInterFilter l₂ c] : CardinalInterFilter (l₁ ⊓ l₂) c := by
+  refine ⟨fun S hSc hS => ?_⟩
+  choose s hs t ht hst using hS
+  replace hs : (⋂ i ∈ S, s i ‹_›) ∈ l₁ := (cardinal_bInter_mem hSc).2 hs
+  replace ht : (⋂ i ∈ S, t i ‹_›) ∈ l₂ := (cardinal_bInter_mem hSc).2 ht
+  refine mem_of_superset (inter_mem_inf hs ht) (subset_sInter fun i hi => ?_)
+  rw [hst i hi]
+  apply inter_subset_inter <;> exact iInter_subset_of_subset i (iInter_subset _ _)
+
+instance cardinalInterFilter_inf (l₁ l₂ : Filter α) {c₁ c₂ : Cardinal.{u}}
+    [CardinalInterFilter l₁ c₁] [CardinalInterFilter l₂ c₂] : CardinalInterFilter (l₁ ⊓ l₂)
+    (c₁ ⊓ c₂) := by
+  have : CardinalInterFilter l₁ (c₁ ⊓ c₂) :=
+    CardinalInterFilter.of_cardinalInterFilter_of_le l₁ inf_le_left
+  have : CardinalInterFilter l₂ (c₁ ⊓ c₂) :=
+    CardinalInterFilter.of_cardinalInterFilter_of_le l₂ inf_le_right
+  exact cardinalInterFilter_inf_eq _ _
+
+/-- Supremum of two `CardinalInterFilter`s is a `CardinalInterFilter`. -/
+instance cardinalInterFilter_sup_eq (l₁ l₂ : Filter α) [CardinalInterFilter l₁ c]
+    [CardinalInterFilter l₂ c] : CardinalInterFilter (l₁ ⊔ l₂) c := by
+  refine ⟨fun S hSc hS => ⟨?_, ?_⟩⟩ <;> refine (cardinal_sInter_mem hSc).2 fun s hs => ?_
+  exacts [(hS s hs).1, (hS s hs).2]
+
+instance cardinalInterFilter_sup (l₁ l₂ : Filter α) {c₁ c₂ : Cardinal.{u}}
+    [CardinalInterFilter l₁ c₁] [CardinalInterFilter l₂ c₂] :
+    CardinalInterFilter (l₁ ⊔ l₂) (c₁ ⊓ c₂) := by
+  have : CardinalInterFilter l₁ (c₁ ⊓ c₂) :=
+    CardinalInterFilter.of_cardinalInterFilter_of_le l₁ inf_le_left
+  have : CardinalInterFilter l₂ (c₁ ⊓ c₂) :=
+    CardinalInterFilter.of_cardinalInterFilter_of_le l₂ inf_le_right
+  exact cardinalInterFilter_sup_eq _ _
+
+variable (g : Set (Set α))
+
+/-- `Filter.CardinalGenerateSets c g` is the (sets of the)
+greatest `cardinalInterFilter c` containing `g`.-/
+inductive CardinalGenerateSets : Set α → Prop
+  | basic {s : Set α} : s ∈ g → CardinalGenerateSets s
+  | univ : CardinalGenerateSets univ
+  | superset {s t : Set α} : CardinalGenerateSets s → s ⊆ t → CardinalGenerateSets t
+  | sInter {S : Set (Set α)} :
+    (#S < c) → (∀ s ∈ S, CardinalGenerateSets s) → CardinalGenerateSets (⋂₀ S)
+
+/-- `Filter.cardinalGenerate c g` is the greatest `cardinalInterFilter c` containing `g`.-/
+def cardinalGenerate (hc : 2 < c) : Filter α :=
+  ofCardinalInter (CardinalGenerateSets g) hc (fun _ => CardinalGenerateSets.sInter) fun _ _ =>
+    CardinalGenerateSets.superset
+
+lemma cardinalInter_ofCardinalGenerate (hc : 2 < c) :
+    CardinalInterFilter (cardinalGenerate g hc) c := by
+  delta cardinalGenerate;
+  apply cardinalInter_ofCardinalInter _ _ _
+
+variable {g}
+
+/-- A set is in the `cardinalInterFilter` generated by `g` if and only if
+it contains an intersection of `c` elements of `g`. -/
+theorem mem_cardinaleGenerate_iff {s : Set α} {hreg : c.IsRegular} :
+    s ∈ cardinalGenerate g (IsRegular.nat_lt hreg 2) ↔
+    ∃ S : Set (Set α), S ⊆ g ∧ (#S < c) ∧ ⋂₀ S ⊆ s := by
+  constructor <;> intro h
+  · induction' h with s hs s t _ st ih S Sct _ ih
+    · refine ⟨{s}, singleton_subset_iff.mpr hs, ?_⟩
+      norm_num; exact ⟨IsRegular.nat_lt hreg 1, subset_rfl⟩
+    · exact ⟨∅, ⟨empty_subset g, mk_eq_zero (∅ : Set <| Set α) ▸ IsRegular.nat_lt hreg 0, by simp⟩⟩
+    · exact Exists.imp (by tauto) ih
+    choose T Tg Tct hT using ih
+    refine ⟨⋃ (s) (H : s ∈ S), T s H, by simpa,
+      (Cardinal.card_biUnion_lt_iff_forall_of_isRegular hreg Sct).2 Tct, ?_⟩
+    apply subset_sInter
+    apply fun s H => subset_trans (sInter_subset_sInter (subset_iUnion₂ s H)) (hT s H)
+  rcases h with ⟨S, Sg, Sct, hS⟩
+  have : CardinalInterFilter (cardinalGenerate g (IsRegular.nat_lt hreg 2)) c :=
+    cardinalInter_ofCardinalGenerate _ _
+  exact mem_of_superset ((cardinal_sInter_mem Sct).mpr
+    (fun s H => CardinalGenerateSets.basic (Sg H))) hS
+
+theorem le_cardinalGenerate_iff_of_cardinalInterFilter {f : Filter α} [CardinalInterFilter f c]
+    (hc : 2 < c) : f ≤ cardinalGenerate g hc ↔ g ⊆ f.sets := by
+  constructor <;> intro h
+  · exact subset_trans (fun s => CardinalGenerateSets.basic) h
+  intro s hs
+  induction' hs with s hs s t _ st ih S Sct _ ih
+  · exact h hs
+  · exact univ_mem
+  · exact mem_of_superset ih st
+  exact (cardinal_sInter_mem Sct).mpr ih
+
+/-- `cardinalGenerate g hc` is the greatest `cardinalInterFilter c` containing `g`.-/
+theorem cardinalGenerate_isGreatest (hc : 2 < c) :
+    IsGreatest { f : Filter α | CardinalInterFilter f c ∧ g ⊆ f.sets } (cardinalGenerate g hc) := by
+  refine ⟨⟨cardinalInter_ofCardinalGenerate _ _, fun s => CardinalGenerateSets.basic⟩, ?_⟩
+  rintro f ⟨fct, hf⟩
+  rwa [le_cardinalGenerate_iff_of_cardinalInterFilter]
+
 end Filter

Mathlib/Order/Filter/CountableInter.lean

@@ -131,52 +131,55 @@ theorem EventuallyEq.countable_bInter {ι : Type*} {S : Set ι} (hS : S.Countabl
 /-- Construct a filter with countable intersection property. This constructor deduces
 `Filter.univ_sets` and `Filter.inter_sets` from the countable intersection property. -/
 def Filter.ofCountableInter (l : Set (Set α))
-    (hp : ∀ S : Set (Set α), S.Countable → S ⊆ l → ⋂₀ S ∈ l)
+    (hl : ∀ S : Set (Set α), S.Countable → S ⊆ l → ⋂₀ S ∈ l)
     (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) : Filter α where
   sets := l
-  univ_sets := @sInter_empty α ▸ hp _ countable_empty (empty_subset _)
+  univ_sets := @sInter_empty α ▸ hl _ countable_empty (empty_subset _)
   sets_of_superset := h_mono _ _
   inter_sets {s t} hs ht := sInter_pair s t ▸
-    hp _ ((countable_singleton _).insert _) (insert_subset_iff.2 ⟨hs, singleton_subset_iff.2 ht⟩)
+    hl _ ((countable_singleton _).insert _) (insert_subset_iff.2 ⟨hs, singleton_subset_iff.2 ht⟩)
 #align filter.of_countable_Inter Filter.ofCountableInter
 
 instance Filter.countableInter_ofCountableInter (l : Set (Set α))
-    (hp : ∀ S : Set (Set α), S.Countable → S ⊆ l → ⋂₀ S ∈ l)
+    (hl : ∀ S : Set (Set α), S.Countable → S ⊆ l → ⋂₀ S ∈ l)
     (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) :
-    CountableInterFilter (Filter.ofCountableInter l hp h_mono) :=
-  ⟨hp⟩
+    CountableInterFilter (Filter.ofCountableInter l hl h_mono) :=
+  ⟨hl⟩
 #align filter.countable_Inter_of_countable_Inter Filter.countableInter_ofCountableInter
 
 @[simp]
 theorem Filter.mem_ofCountableInter {l : Set (Set α)}
-    (hp : ∀ S : Set (Set α), S.Countable → S ⊆ l → ⋂₀ S ∈ l) (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l)
-    {s : Set α} : s ∈ Filter.ofCountableInter l hp h_mono ↔ s ∈ l :=
+    (hl : ∀ S : Set (Set α), S.Countable → S ⊆ l → ⋂₀ S ∈ l) (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l)
+    {s : Set α} : s ∈ Filter.ofCountableInter l hl h_mono ↔ s ∈ l :=
   Iff.rfl
 #align filter.mem_of_countable_Inter Filter.mem_ofCountableInter
 
 /-- Construct a filter with countable intersection property.
 Similarly to `Filter.comk`, a set belongs to this filter if its complement satisfies the property.
 Similarly to `Filter.ofCountableInter`,
 this constructor deduces some properties from the countable intersection property
-which becomes the countable union property because we take complements of all sets.
-
-Another small difference from `Filter.ofCountableInter`
-is that this definition takes `p : Set α → Prop` instead of `Set (Set α)`. -/
-def Filter.ofCountableUnion (p : Set α → Prop)
-    (hUnion : ∀ S : Set (Set α), S.Countable → (∀ s ∈ S, p s) → p (⋃₀ S))
-    (hmono : ∀ t, p t → ∀ s ⊆ t, p s) : Filter α := by
-  refine .ofCountableInter {s | p sᶜ} (fun S hSc hSp ↦ ?_) fun s t ht hsub ↦ ?_
+which becomes the countable union property because we take complements of all sets. -/
+def Filter.ofCountableUnion (l : Set (Set α))
+    (hUnion : ∀ S : Set (Set α), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l)
+    (hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l) : Filter α := by
+  refine .ofCountableInter {s | sᶜ ∈ l} (fun S hSc hSp ↦ ?_) fun s t ht hsub ↦ ?_
   · rw [mem_setOf_eq, compl_sInter]
-    exact hUnion _ (hSc.image _) (forall_mem_image.2 hSp)
-  · exact hmono _ ht _ (compl_subset_compl.2 hsub)
-
-instance Filter.countableInter_ofCountableUnion (p : Set α → Prop) (h₁ h₂) :
-    CountableInterFilter (Filter.ofCountableUnion p h₁ h₂) :=
+    apply hUnion (compl '' S) (hSc.image _)
+    intro s hs
+    rw [mem_image] at hs
+    rcases hs with ⟨t, ht, rfl⟩
+    apply hSp ht
+  · rw [mem_setOf_eq]
+    rw [← compl_subset_compl] at hsub
+    exact hmono sᶜ ht tᶜ hsub
+
+instance Filter.countableInter_ofCountableUnion (l : Set (Set α)) (h₁ h₂) :
+    CountableInterFilter (Filter.ofCountableUnion l h₁ h₂) :=
   countableInter_ofCountableInter ..
 
 @[simp]
-theorem Filter.mem_ofCountableUnion {p : Set α → Prop} {hunion hmono s} :
-    s ∈ ofCountableUnion p hunion hmono ↔ p sᶜ :=
+theorem Filter.mem_ofCountableUnion {l : Set (Set α)} {hunion hmono s} :
+    s ∈ ofCountableUnion l hunion hmono ↔ l sᶜ :=
   Iff.rfl
 
 instance countableInterFilter_principal (s : Set α) : CountableInterFilter (𝓟 s) :=

Mathlib/SetTheory/Cardinal/Cofinality.lean

@@ -957,6 +957,9 @@ theorem IsRegular.pos {c : Cardinal} (H : c.IsRegular) : 0 < c :=
   aleph0_pos.trans_le H.1
 #align cardinal.is_regular.pos Cardinal.IsRegular.pos
 
+theorem IsRegular.nat_lt {c : Cardinal} (H : c.IsRegular) (n : ℕ) : n < c :=
+  lt_of_lt_of_le (nat_lt_aleph0 n) H.aleph0_le
+
 theorem IsRegular.ord_pos {c : Cardinal} (H : c.IsRegular) : 0 < c.ord := by
   rw [Cardinal.lt_ord, card_zero]
   exact H.pos
@@ -1114,6 +1117,33 @@ theorem sum_lt_of_isRegular {ι : Type u} {f : ι → Cardinal} {c : Cardinal} (
   sum_lt_lift_of_isRegular.{u, u} hc (by rwa [lift_id])
 #align cardinal.sum_lt_of_is_regular Cardinal.sum_lt_of_isRegular
 
+@[simp]
+theorem card_lt_of_card_iUnion_lt {ι : Type u} {α : Type u} {t : ι → Set α} {c : Cardinal}
+    (h : #(⋃ i, t i) < c) (i : ι) : #(t i) < c :=
+  lt_of_le_of_lt (Cardinal.mk_le_mk_of_subset <| subset_iUnion _ _) h
+
+@[simp]
+theorem card_iUnion_lt_iff_forall_of_isRegular {ι : Type u} {α : Type u} {t : ι → Set α}
+    {c : Cardinal} (hc : c.IsRegular) (hι : #ι < c) : #(⋃ i, t i) < c ↔ ∀ i, #(t i) < c := by
+  refine ⟨card_lt_of_card_iUnion_lt, fun h ↦ ?_⟩
+  apply lt_of_le_of_lt (Cardinal.mk_sUnion_le _)
+  apply Cardinal.mul_lt_of_lt hc.aleph0_le
+    (lt_of_le_of_lt Cardinal.mk_range_le hι)
+  apply Cardinal.iSup_lt_of_isRegular hc (lt_of_le_of_lt Cardinal.mk_range_le hι)
+  simpa
+
+theorem card_lt_of_card_biUnion_lt {α β : Type u} {s : Set α} {t : ∀ a ∈ s, Set β} {c : Cardinal}
+    (h : #(⋃ a ∈ s, t a ‹_›) < c) (a : α) (ha : a ∈ s) : # (t a ha) < c := by
+  rw [biUnion_eq_iUnion] at h
+  have := card_lt_of_card_iUnion_lt h
+  simp_all only [iUnion_coe_set,
+    Subtype.forall]
+
+theorem card_biUnion_lt_iff_forall_of_isRegular {α β : Type u} {s : Set α} {t : ∀ a ∈ s, Set β}
+    {c : Cardinal} (hc : c.IsRegular) (hs : #s < c) :
+    #(⋃ a ∈ s, t a ‹_›) < c ↔ ∀ a (ha : a ∈ s), # (t a ha) < c := by
+  rw [biUnion_eq_iUnion, card_iUnion_lt_iff_forall_of_isRegular hc hs, SetCoe.forall']
+
 theorem nfpFamily_lt_ord_lift_of_isRegular {ι} {f : ι → Ordinal → Ordinal} {c} (hc : IsRegular c)
     (hι : Cardinal.lift.{v, u} #ι < c) (hc' : c ≠ ℵ₀) (hf : ∀ (i), ∀ b < c.ord, f i b < c.ord) {a}
     (ha : a < c.ord) : nfpFamily.{u, v} f a < c.ord := by