not_facet_iff_subface — Mathlib

English

A face s is not a facet precisely when there exists a larger face t with s ⊊ t.

Русский

Грань s не является фасетом тогда и только тогда, когда существует грань t, такая что s ⊊ t.

LaTeX

$$s ∈ K.faces → (s ∉ K.facets ↔ ∃ t ∈ K.faces, s ⊂ t)$$

Lean4

theorem not_facet_iff_subface (hs : s ∈ K.faces) : s ∉ K.facets ↔ ∃ t, t ∈ K.faces ∧ s ⊂ t :=
  by
  refine ⟨fun hs' : ¬(_ ∧ _) => ?_, ?_⟩
  · push_neg at hs'
    obtain ⟨t, ht⟩ := hs' hs
    exact ⟨t, ht.1, ⟨ht.2.1, fun hts => ht.2.2 (Subset.antisymm ht.2.1 hts)⟩⟩
  · rintro ⟨t, ht⟩ ⟨hs, hs'⟩
    have := hs' ht.1 ht.2.1
    rw [this] at ht
    exact ht.2.2 (Subset.refl t)

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