ssubset_iff_of_subset

Mathlib.Data.Finset.Defs

URI: https://scilib.ai/kg/mathlib#Finset.ssubset_iff_of_subset

English

If s1 ⊆ s2, then s1 ⊂ s2 iff ∃ x ∈ s2, x ∉ s1.

Русский

Если s1 ⊆ s2, то s1 ⊂ s2 эквивалентно ∃ x ∈ s2, x ∉ s1.

LaTeX

$$$(s_1 \subseteq s_2) \Rightarrow (s_1 \subset s_2 \iff \exists x \in s_2, x \notin s_1)$$$

Lean4

theorem ssubset_iff_of_subset {s₁ s₂ : Finset α} (h : s₁ ⊆ s₂) : s₁ ⊂ s₂ ↔ ∃ x ∈ s₂, x ∉ s₁ :=
  Set.ssubset_iff_of_subset h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru