intent_subset_intent_iff — Mathlib

English

c.intent ⊆ d.intent if and only if d ≤ c.

Русский

c.intent ⊆ d.intent тогда и только тогда, когда d ≤ c.

LaTeX

$$$\forall c,d : \mathrm{Concept}\,\alpha\,\beta\,r,\; c.intent \subseteq d.intent \iff d \le c$$$

Lean4

@[simp]
theorem intent_subset_intent_iff : c.intent ⊆ d.intent ↔ d ≤ c :=
  by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · rw [← extent_subset_extent_iff, ← c.lowerPolar_intent, ← d.lowerPolar_intent]
    exact lowerPolar_anti _ h
  · rw [← c.upperPolar_extent, ← d.upperPolar_extent]
    exact upperPolar_anti _ h

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