isInitSeg_iff_exists_initSeg — Mathlib

English

IsInitSeg 𝒜1 r and IsInitSeg 𝒜2 r imply 𝒜1 ⊆ 𝒜2 or 𝒜2 ⊆ 𝒜1.

Русский

IsInitSeg 𝒜1 r и IsInitSeg 𝒜2 r тогда и только тогда, когда одно множество содержит другое.

LaTeX

$$IsInitSeg(𝒜1, r) ∧ IsInitSeg(𝒜2, r) ⇒ 𝒜1 ⊆ 𝒜2 ∨ 𝒜2 ⊆ 𝒜1$$

Lean4

/-- Being a nonempty initial segment of colex is equivalent to being an `initSeg`. -/
theorem isInitSeg_iff_exists_initSeg : IsInitSeg 𝒜 r ∧ 𝒜.Nonempty ↔ ∃ s : Finset α, #s = r ∧ 𝒜 = initSeg s :=
  by
  refine ⟨fun h𝒜 ↦ h𝒜.1.exists_initSeg h𝒜.2, ?_⟩
  rintro ⟨s, rfl, rfl⟩
  exact ⟨isInitSeg_initSeg, initSeg_nonempty⟩

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