Theorems · Theorem · logic and foundations

Set.exists_subsuperset_card_eq

∀ {α : Type u_1} {s t : Set α} {n : ℕ}, s ⊆ t → s.ncard ≤ n → n ≤ t.ncard → ∃ u, s ⊆ u ∧ u ⊆ t ∧ u.ncard = n

Given a subset s of a set t, of sizes at most and at least n respectively, there exists a set u of size n which is both a superset of s and a subset of t.

Defined in

Mathlib.Data.Set.Card

Cited by

1 results in Mathlib

Foundations

Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound