card_le_card_of_forall_subsingleton

English

As above

Русский

Если для каждого a ∈ s существует b ∈ t с r a b, и для каждого b ∈ t множество {a ∈ s | r a b} является подселедом, то |s| ≤ |t|.

LaTeX

$$$$ \forall a \in s, \exists b \in t, r(a,b) \quad \text{and} \quad \forall b \in t, \{a \in s \mid r(a,b)\} \text{ Subsingleton} \Rightarrow |s| \le |t| $$$$

Lean4

theorem card_le_card_of_forall_subsingleton (hs : ∀ a ∈ s, ∃ b, b ∈ t ∧ r a b)
    (ht : ∀ b ∈ t, ({a ∈ s | r a b} : Set α).Subsingleton) : #s ≤ #t := by
  classical
  rw [← mul_one #s, ← mul_one #t]
  exact
    card_mul_le_card_mul r
      (fun a h ↦
        card_pos.2
          (by
            rw [← coe_nonempty, coe_bipartiteAbove]
            exact hs _ h : (t.bipartiteAbove r a).Nonempty))
      (fun b h ↦
        card_le_one.2
          (by
            simp_rw [mem_bipartiteBelow]
            exact ht _ h))

Похожие утверждения