card_le_card_of_forall_subsingleton'

English

Swap the roles of a and b in the earlier subsingleton bound, obtaining |t| ≤ |s| under the swapped relation.

Русский

Поменяв роли a и b в предыдущее ограничение subsingleton, получаем |t| ≤ |s| при поменянном отношении.

LaTeX

$$$$ |t| \le |s| $$$$

Lean4

theorem card_le_card_of_forall_subsingleton' (ht : ∀ b ∈ t, ∃ a, a ∈ s ∧ r a b)
    (hs : ∀ a ∈ s, ({b ∈ t | r a b} : Set β).Subsingleton) : #t ≤ #s :=
  card_le_card_of_forall_subsingleton (swap r) ht hs

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