covBy_iff_card_sdiff_eq_one — Mathlib

English

Let t ⋖ s. Then t ⊆ s and |s \\ t| = 1; conversely, if t ⊆ s and |s \\ t| = 1, then t ⋖ s.

Русский

Пусть t ⋖ s. Тогда t ⊆ s и |s \ t| = 1; обратно, если t ⊆ s и |s \ t| = 1, тогда t ⋖ s.

LaTeX

$$$ t \\ CovBy s \\iff (t \\subseteq s) \\land (s \\setminus t).card = 1 $$$

Lean4

theorem covBy_iff_card_sdiff_eq_one : t ⋖ s ↔ t ⊆ s ∧ (s \ t).card = 1 :=
  by
  rw [covBy_iff_exists_insert]
  constructor
  · rintro ⟨a, ha, rfl⟩
    simp [*]
  · simp_rw [card_eq_one]
    rintro ⟨hts, a, ha⟩
    refine ⟨a, (mem_sdiff.1 <| superset_of_eq ha <| mem_singleton_self _).2, ?_⟩
    rw [insert_eq, ← ha, sdiff_union_of_subset hts]

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