Skip to content

Commit

Permalink
fix(data/finset): remove partial_order instance
Browse files Browse the repository at this point in the history
* The partial_order instance is subsumed by the lattice instance.
* The other two iff.rfl theorems do not seem necessary.
  • Loading branch information
spl committed Jun 28, 2018
1 parent 2d9041d commit f499e72
Showing 1 changed file with 0 additions and 10 deletions.
10 changes: 0 additions & 10 deletions data/finset.lean
Expand Up @@ -75,16 +75,6 @@ theorem subset_iff {s₁ s₂ : finset α} : s₁ ⊆ s₂ ↔ ∀ ⦃x⦄, x

instance : has_ssubset (finset α) := ⟨λa b, a ⊆ b ∧ ¬ b ⊆ a⟩

instance : partial_order (finset α) :=
{ le := (⊆),
lt := (⊂),
le_refl := subset.refl,
le_trans := @subset.trans _,
le_antisymm := @subset.antisymm _ }

@[simp] theorem le_iff_subset {s₁ s₂ : finset α} : s₁ ≤ s₂ ↔ s₁ ⊆ s₂ := iff.rfl
@[simp] theorem lt_iff_ssubset {s₁ s₂ : finset α} : s₁ < s₂ ↔ s₁ ⊂ s₂ := iff.rfl

@[simp] theorem val_lt_iff {s₁ s₂ : finset α} : s₁.1 < s₂.1 ↔ s₁ ⊂ s₂ :=
and_congr val_le_iff $ not_congr val_le_iff

Expand Down

0 comments on commit f499e72

Please sign in to comment.